Сделай Сам Свою Работу на 5

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





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

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

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

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

КНФ(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. Упрощение формул с помощью законов

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

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

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 « A1 Ú … Ú Ak Ú (ØB1) Ú … Ú (ØBl)

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

S « (A1 Ú … Ú Ak) Ú Ø(B1 Ù … Ù Bl)

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

S « (B1 Ù … Ù Bl) ® (A1 Ú … Ú Ak)

S « (A1 Ú … Ú Ak) (B1 Ù … Ù Bl)

Или

S « A1 ; … ; Ak : - B1 , … , Bl

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

S « A1 : - B1 , … , Bl

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

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



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

D=(C1 \ {L}) U (C2 \ {ØL})

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

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

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

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

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

R(S)=S U {R({C1, C2 }), R({C1, C3 }), R({C2, C3})}

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

 

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

либо Ci Î S;

либо Ci = R({Cj, Ck}), 1<=j,k<=i

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

C1,…,Cn, C

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

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

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

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

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

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

3. C3=R({C1, C2})={ØA, ØB, ØA, ØB}={ØA, ØB}

4. C4={A, ØB}

5. C5=R({C3, C4})={ØB}

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

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

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

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

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

 








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



©2015 - 2024 stydopedia.ru Все материалы защищены законодательством РФ.