Формальное определение метода резолюций

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

Метод резолюций – наиболее эффективный метод алгоритмического доказательства в логике высказываний (и в логике предикатов 1-го порядка). Метод резолюций составляет основу языка логического программирования ПРОЛОГ, как и метод семантических таблиц Бета, строит доказательство путем опровержения.

«Быстрый» алгоритм приведения высказывания к конъюнктивной нормальной форме (КНФ)

Пусть F — высказывание, содержащее атомы A₁, … , A_n.

КНФ(F): ,

где – атом или отрицание атома F.

Литерал – произвольный атом или его отрицание (A,B, ØC).

Алгоритм состоит в выполнении следующих операций (неформальное описание) для высказывания F:

1. Избавляемся от операций {«, ®} с помощью законов

(A«B) « (A®B)Ù(B®A)

(A®B) « (ØA Ú B)

2. Вносим отрицания внутрь скобок (продвижение знака отрицания до атома) с помощью законов де Моргана

Ø(A Ù B) « (ØA Ú ØB)

Ø(A Ú B) « (ØA Ù ØB)

3. Собираем вместе литералы одного и того же атома (для дальнейшего упрощения формул) с помощью свойств ассоциативности Ù и Ú

(A Ú (B Ú C)) « ((A Ú B) Ú C)

(A Ù (B Ù C)) « ((A Ù B) Ù C)

с помощью свойства коммутативности Ù и Ú

A Ú B « B Ú A

A Ù B « B Ù A

с помощью свойств дистрибутивности Ù относительно Ú и Ú относительно Ù

(A Ú (B Ù C)) « ((A Ú B) Ù (A Ú C))

(A Ù (B Ú C)) « ((A Ù B) Ú (A Ù C))

4. Упрощение формул с помощью законов

Пример. Представить следующее высказывание в КНФ:

S: Ø((A Ú B) Ù (ØA Ú ØB)) Ù C

Шаг 1. Используя законы де Моргана, вносим отрицания внутрь скобок:

S: (Ø(A Ú B) Ú (Ø(ØA Ú ØB)) Ù C

S: ((ØA Ù ØB) Ú (ØØA Ù ØØB)) Ù C

Шаг 2. Упрощаем

S: ((ØA Ù ØB) Ú (A Ù B)) Ù C

Шаг 3. Используем дистрибутивность

S: (((ØA Ù ØB) Ú A) Ù ((ØA Ù ØB) Ú B)) Ù C

S: (((ØA Ú A) Ù (ØB Ú A)) Ù ((ØA Ú B) Ù (ØB Ú B))) Ù C

Шаг 4. Упрощаем

S: ((ØB Ú A) Ù (ØA Ú B)) Ù C (КНФ)

Теоретико-множественная форма представления высказываний

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

Высказывание (дизъюнкт): ØB Ú A Ú ØC Ú D

Теоретико-множественное представление дизъюнкта: {ØB, A, ØC, D}

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

Высказывание в КНФ (конъюнкция дизъюнктов):

((ØB Ú A) Ù (ØA Ú B)) Ù C

Теоретико-множественное представление высказывания в виде множества дизъюнктов:

{{ØB, A}, {ØA, B}, {C}}

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

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

Система обозначений в логическом программировании

Пусть S – высказывание (дизъюнкция литералов)

S « A₁ Ú … Ú A_k Ú (ØB₁) Ú … Ú (ØB_l)

Применяя закон де Моргана, получим

S « (A₁ Ú … Ú A_k) Ú Ø(B₁ Ù … Ù B_l)

Используя тавтологию (B®A) « (A Ú ØB), можно записать

S « (B₁ Ù … Ù B_l) ® (A₁ Ú … Ú A_k)

S « (A₁ Ú … Ú A_k) (B₁ Ù … Ù B_l)

Или

S « A₁ ; … ; A_k : - B₁ , … , B_l

Определение.Дизъюнкт S вида (k=1)

S « A₁ : - B₁ , … , B_l

называется хорновским дизъюнктом.

A₁ – называется целью (заголовком) S

B_l - называются хвостом, телом или подцелями.

Содержательное истолкование хорновского дизъюнкта таково: для того, чтобы цель А была истинна, достаточно, чтобы все подцели B₁ , … , B_l были также истинны.

При k=0 дизъюнкт : - B₁ , … , B_l называется целью программы (или запросом к программе). Интерпретируется как гипотеза, требующая подтверждения: верно ли, что высказывание B₁ Ù … Ù B_l истинно?

При l=0 дизъюнкт A₁ : - называется фактом, не требующим подтверждения. Совокупность таких фактов образует базу фактов пролог - программы.

Понятие резолюции

Резолюция представляет собой дедуктивное правило, позволяющее нам выводить дизъюнктивное высказывание из двух других дизъюнктивных высказываний.

Пример. Рассмотрим множество дизъюнктов: {{ØА,В}, {А,С}}. Используя резолюцию, из этого множества мы можем вывести дизъюнкт {B, C}.

Можно считать, что дизъюнкты {ØА,В} и {А,С} вступают в противоречие, поскольку содержат ØА и A. Резолюция (от английского слова resolve – разрешать) разрешает конфликт, устраняя причину противоречия (т.е. литералы A и ØА). Резолюция представляет собой правило логического вывода следующего вида:

{{ØА,В}, {А,С}} ⊢ {B, C}.

Переформулируем вышеозначенные дизъюнкты в классической формулировке логики высказываний:

Исходные дизъюнкты имеют вид: (ØАÚВ), (AÚC)

Множеству дизъюнктов соответствует высказывание: (ØАÚВ)Ù(AÚC)

Откуда выводится высказывание: BÚC

Это означает, что имеет место тавтология:

(ØАÚВ)Ù(AÚC) ® (BÚC)

Формальное определение метода резолюций

Определение. Пусть C₁ и C₂ – дизъюнкты, L – литерал, причем LÎ C₁, ØLÎ C₂. Тогда резольвентой дизъюнктов C₁ и C₂ называется дизъюнкт

D=(C₁ \ {L}) U (C₂ \ {ØL})

Определение. (Множество резольвент) Пусть S={C₁,…,C_n} – множество дизъюнктов. Множество

R(S)=S U {D : D – резольвента дизъюнктов C_i и C_j, 1<= i,j <=n}

называется резольвентой множества S.

Обозначим через R({C_i, C_j}) резольвенту дизъюнктов C_i и C_j

Пример. Пусть S={{A, ØB, ØC},{B,D},{ØA, ØD}} –множество дизъюнктов. Резольвента множества S будет иметь вид (построить):

R(S)=S U {R({C₁, C₂ }), R({C₁, C₃ }), R({C₂, C₃})}

R(S)=S U {{ A, ØC, D }, { ØB, ØC, ØD}, { B,ØA }}

Определение (доказательства методом резолюций). Пусть S – множество дизъюнктов. Резолютивным выводом из S называется такая конечная последовательность дизъюнктов C₁,…,C_n , что для любого дизъюнкта C_i i=1..n верно, что

либо C_i Î S;

либо C_i = R({C_j, C_k}), 1<=j,k<=i

Определение. Дизъюнкт C является резолютивно выводимым из множества дизъюнктов S (S ⊢_R C), если существует резолютивный вывод из S вида

C₁,…,C_n, C

Пример. Рассмотрим высказывание S: (A Ú ØB) Ù (ØA Ú ØB Ú ØC) Ù (ØA Ú ØB Ú C). Требуется доказать, что высказывание ØB резолютивно выводимо из S.

· Представим S в виде множества дизъюнктов

{{A, ØB},{ØA, ØB, ØC},{ØA, ØB, C}}

· Построим резолютивный вывод

1. C₁={ØA, ØB, ØC}

2. C₂={ØA, ØB, C}

3. C₃=R({C₁, C₂})={ØA, ØB, ØA, ØB}={ØA, ØB}

4. C₄={A, ØB}

5. C₅=R({C₃, C₄})={ØB}

Пример. Рассмотрим высказывание S: (A«(B®C)) Ù (A«B) Ù (A« ØC). Требуется доказать методом резолюций, что S – неподтверждаемо.

Что нужно сделать:

1. Представить S в виде множества дизъюнктов

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

(Как получается пустой дизъюнкт, например так: ð=R({{B},{ØB}}))

Не нашли, что искали? Воспользуйтесь поиском по сайту: