Материал: Методичка Дзержинский

высказывания.

При доказательстве высказываний из аксиом мы рассматриваем различные комбинации высказываний ,пытаясь определить такую которая позволяет подходящим образом применить правило вывода. В результате вывод оказывается сложным и продолжительным.

Метод резолюции

Метод резолюции – наиболее эффективный способ алгоритмического доказательства как в логике высказываний так и в логике предикатов именно этот метод построения доказательств составляет основу языка программирования ПРОЛОГ

Мы знаем что любую формулу не являющуюся тавтологией можно представить в виде КНФ.

Определение. Латерал – это произвольный атом или его отрицание. Дизъюнкция конечного множества литералов называется дизъюнктом Пустой дизъюнкт – это дизъюнкт который не содержит ни одного

литерала и является всегда неподтверждённым.

Удобнее формулировать сложное высказывание, представленное в виде КНФ как множество дизъюнктов . А каждый дизъюнкт представлять как множество литералов. ТО есть КНФ это конъюнкция конечного множества дизъюнктов , а дизъюнкт – это дизъюнкция конечного множества литералов.

Пример (Av¬Bv¬C) ^(BvD)^( ¬Av¬D) S={{{A, ┐B, ┐C},{B,D},{┐A, ┐D}}

Напомним свойства операций v и ^: Склеивание дизъюнкций

(XvD)*( ¬XvD)=(X*¬X)vD=0vD=D

Поглощение

D1*(D1vD2)=(D1v0)*( D1vD2)= D1v(0*D2)=D1v0=D1

Обобщённое склеивание

(XvD1)*( ¬XvD2)=(XvD1)*( ¬XvD2)*(D1vD2)

Доказательство этого

(XvD1)*( ¬XvD2)=(XvD1)*(XvD1vD2)*( ¬XvD2)*( ¬XvD2vD1)=(XvD1)*( ¬XvD2)*(XvD1vD2)( ¬XvD2vD1)=

=(XvD1)*( ¬XvD2)*(D1vD2)

XvD1

D1vD2

¬XvD2

Пусть С1 и С2 – дизъюнкты, такие что C1 ={L}υA a C2={¬L}υB

31

Мы можем считать, что дизъюнкты С1 и С2 вступают в противоречие, так как С1 содержит литерал L a C2 – литерал - ¬L.Устранение причины противоречия приводит к дизъюнкту D=AυB, который разрешает конфликт. Своим названием метод резолюции обязан этому разрешению (от англ. Resolve

– разрешать)

Дадим формальное определение резолюции

Опр Пусть С1 и С2 дизъюнкты, L- такой литерал, что L ϵ C1 и ¬L ϵ C2, тогда резольвентой дизъюнктов С1 и С2 называется дизъюнкт

D={C1\{L}}υ{C2\{¬L}

D={AυB}

Опр Пусть мн. S={C1,….Cn} – множество дизъюнктов. Резольвентой мн S наз множество R(S)=Sυ{D:D-резольвента дизъюнктов Ci,Cj 1≤i,j≤n}

Пример S={{A, ¬B, ¬C},{B,D},{¬A, ¬D}}

В итоге R(S)= {B,D},{¬A, ¬D},{A,D, ¬C},{B¬A},{¬B, ¬C, ¬D}

Мы можем продолжить применять этот метод последовательно получим множества

R0 (S)=S,R1(S)=R0(S) υR(S), R2(S)=R1(S) υR(R1S …Rn(S)= Rn-1(S) υR(Rn-

1(S))

А затем объединив все множества

R*(S)=

Заметим, что R*(S) конечно тогда и только тогда, когда S конечно

Содержательная подоплёка метода резолюции такова: если истинное означивание подтверждает дизъюнкты С1 и С2 , то оно также подтверждает их резольвенту D. Аналогично, если истинностное означивание подтверждает мн. S, то оно также подтверждает R(S).

Применим резолюцию: D={A} –резольвент не содержит никакой информации о литерале В

Опр. Пусть S – множество дизъюнктов. Резолюционным выводом из S

32

назовём такую конечную последовательность дизъюнктов С1,....Сn , что для каждого Ci i=1,…n

Либо Ci ϵ S, либо Ci ϵ R({Cj,Cк}) 1≤j, k≤I

Дизъюнкт C считается резолютивно выводимым из мн. дизъюнктов S, если существует резолютивный вывод из S, последний дизъюнкт которого – С=Cn. Очевидно что C ϵ R*(S). Этот факт обозначается так

S R С

Мн дизъюнктов S не подтверждаемо (или невыполнимо) тогда и только тогда,

Когда R*(S)= содержит пустой дизъюнкт

То есть если мы при применении метода резолюции к множеству S получим пустой дизъюнкт, то множество S будет неподтверждаемым .

Так как правило резолюции – это выводимое правило логики высказываний, то можно использовать теорему дедукции, по которой

{SυK} ⱶ ¬ L ↔ S ⱶ (К→L)

{Sυ¬B} ⱶ □ ↔ S ⱶ (¬B →□)

{Sυ¬B } ⱶ □ ↔ S ⱶ ¬¬B v □

S ⱶ B ↔ (Sυ ¬B) ⱶ □

Пример. Доказать, что высказывание ┐B резолютивно выводимо из мн

S={{A, ┐B},{¬A, ¬B, ¬C},{¬A, ¬B,C}}

Пример. Дано выск азывание

(CA ↔ (B→C))^(A↔B)^A(↔┐C))

Докажите что оно не подтверждаемо (или невыполнимо).

Исчисление предикатов

Опр. Пусть x1,x2,….xn – символы переменных произвольной природы.

33

Наборы переменных (x1,…,xn) принадлежат множеству S2, которое будем называть предметной областью, а переменные будем называть предметами. N- местным предикатом, определённым на предметной области S2, называют отображение S2 во множестве высказываний.

То есть это утверждение о предметных переменных обладающее свойством, что при фиксации значений всех переменных об этом утверждении можно сказать, истинно оно или ложно

P(x,y,z) = “ x2 + y2 ≤ z2; x,y,z ϵ R “- трёхместный предикат определённый

на R3

D(x1,x2) = “натуральное число x1 делится без остатка на натуральное число x2” – двухместный предикат определённый на множестве пор натуральных чисел D(6,3)=И D(5,2)=Л

Множеством истинности предиката наз:

P-1({И}) = {(x1,…,xn) ϵ S2/ P(x2,…,xn) = И}

Множеством ложности предиката наз:

P-1({Л}) = {(x1,…,xn) ϵ S2/ P(x2,…,xn) = Л}

Предикат P, определённый на S2 наз тождественно истинным, если P- 1({И}) = S2

Тождественно ложным. если P-1({Л}) = S2

Нетривиально выполнимым если P-1({И}) ≠ ø и P-1({Л}) ≠ ø

Поскольку предикаты – это отображения со значениями во множестве высказываний, где введены логические операции, то эти операции естественно определяются и для предикатов.

Утверждение. Множество n- местных предикатов, определённых на S2 образует булеву алгебру предикатов, т е для них справедливы все аксиомы булевых алгебр (свойства операций)

Фиксация значений переменных: пусть Р(x1,…,xn) n местный предикат, определённый на S2. Зафиксируем xi=a (1≤i≤n). Получим n-1 местный предикат.

Q(x1,…,xi-1, xi+1…,xn)≡P(x1,…, xi-1,a, xi+1,…,xn)

Определённый на мн S2ia значений переменных x1,…, xi-1, xi+1,…xn

Пример P(x,y,z) = x2 + y2 ≤ z2; x,y,z ϵ R3 зафиксируем z=2 получим “ x2 +

34

y2 ≤ 4” (x,y) ϵ R2

Навешивание кванторов:

Окр. Пусть P(x) – одноместный предикат. Поставим ему в соответствие высказывание, обозначаемое xP(x) (для любого x P(x)), которое истинно тогда и только тогда, когда P(x) тождественно истинный предикат.

О высказывании xP(x) говорят, что оно получено из предиката Р навешиванием квантора всеобщности из переменной х

Опр. Когда Р(х) – одноместный предикат. Поставим ему в соответствие высказывание, обозначаемое xP(x) (существует х Р(х)), которое ложно тогда и только тогда, когда Р(х) тождественно ложный предикат. О высказывании xP(x) говорят, что оно получено из предиката Р навешиванием квантора по переменной х.

Квантор всеобщности обобщает конъюнкцию, а квантор существования – дизъюнкцию в случае предикатов, определённых на бесконечных множествах.

Те играют роль бесконечности конъюнкций и дизъюнкций

Аесли Р(х) – одноместный предикат определённый на конечном множестве S2 = {a1;a2;a3;…;an)

Тогда справедливо :

xP(x) ≡ Р(a1)^P(a2)^…^P(an)

xP(x) ≡ Р(a1)vP(a2)v…vP(an)

Доказательство очевидно из определения кванторов и логических операций.

Замечания 1 Высказывание можно считать предикатами, не содержащими переменных, т е

0-местными предикатами

2 Кванторы можно рассматривать как отображения уменьшающиеся местность на 1

3 Формулы алгебры высказываний от n высказывательных переменных можно рассматривать как n-местные предикаты от этих переменных.

Пусть Р(х1,...,хn) – n-местный предикат, определённый на S2 зафиксируем в нем значения переменных x1, xi-1, xi+1,xn на полученной одноместный предикат Q(xi) навесим квантор всеобщности (или существования), получим высказывание. Сопоставления любому набору значений переменных x1,…, xi-1, xi+1,…,xn вполне определённого высказывания

35