Практика по методу резолюции

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

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

Дж. Робинсон показал, что выводимость формулы Ф из множества посылок и аксиом А, В, С, … равносильна доказательству теоремы: (А&В&С&…ØФ)=л. Покажем обоснованность такого предположения:

1) Запишем формулу связи импликации и выводимости логической формулы:

|- (А&В&С&…®Ф)

2) Избавимся от импликации:

|- (Ø(А&В&С&…)ÚФ)

3) Применим закон де Моргана:

|- Ø (А&В&С&…&ØФ)

4) Поскольку данная формула выводима (знак |-), верна формула

Ø (А&В&С&…&ØФ)=и,

следовательно, (А&B&C&…&ØФ)=л.

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

Назовем два дизъюнкта, содержащие одинаковые ПП, но с противоположными знаками, контрарными атомами.

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

Шаг 1: принять отрицание заключения, т.е. ¬Ф,

Шаг 2: привести все формулы посылок и отрицания заключения в КНФ,

Шаг 3: сформировать множество К дизъюнктов всех посылок и отрицания заключения: K = {D₁, D₂, …, D_k},

Шаг 4: выполнить анализ пар множества K по правилу: если существует пара элементов, содержащих контрарные атомы, то соединить эту пару логической связкой дизъюнкции и сформировать новый дизъюнкт - резольвенту, исключив из нее контрарные атомы,

Шаг 5: если в результате соединения дизъюнктов будет получена пустая резольвента – аналог ложности формулы (обозначается ), то конец, т.к. доказательство подтвердило истинность заключения. Иначе включить резольвенту в множество дизъюнктов K и перейти к шагу 4. При этом по закону идемпотентности любой дизъюнкт и любую резольвенту можно использовать неоднократно, т.е. из множества К не следует удалять использованные в соединении дизъюнкты.

1. Доказать истинность заключения:

(А&В®С),(С&D®ØM),(ØN®D&M)

(A&B®N)

Решение:

1. Выполним отрицание заключения:

Ø(A&B®N)=Ø(Ø(А&B)ÚN)=(A&B&ØN)

2. Формируем КНФ из посылок:

А&В®С=Ø(А&В)ÚС=(ØАÚØВÚС) – элементарная дизъюнкция

С&D®ØM=Ø(С&D)ÚØM= (ØCÚØDÚØM) – элементарная дизъюнкция

ØN®D&M=ØØNÚD&M= (NÚD)&(NÚM)

3. Формируем множество элементарных дизъюнкций К:

К={(ØАÚØВÚС), (ØCÚØDÚØM), (NÚD), (NÚM), А, B, ØN}

4. Формирование резольвент (объединяемые дизъюнкты, содержащие контрарные атомы, здесь и далее показаны полужирным курсивом):

К={(ØАÚØВÚС),(ØCÚØDÚØM),(NÚD), (NÚM),А,B, ØN }=

{(ØАÚØВÚС), (ØCÚØDÚØM), (NÚD), (NÚM), А, B,ØN, M }=

{ (ØАÚØВÚС),(ØCÚØDÚØM),(NÚD),(NÚM),А,B,ØN,М, (ØCÚØD) }=

{(ØАÚØВÚС),(ØCÚØDÚØM),(NÚD),(NÚM), А,B,ØN,М,(ØCÚØD), (ØAÚØBÚØD) }=

{(ØАÚØВÚС),(ØCÚØDÚØM),(NÚD),(NÚM),А, B,ØN,М,(ØCÚØD),(ØAÚØBÚØD), (ØBÚØD) }=

{(ØАÚØВÚС),(ØCÚØDÚØM), (NÚD),(NÚM),А,B,ØN,М,(ØCÚØD),(ØAÚØBÚØD),(ØBÚØD), ØD }=

{(ØАÚØВÚС),(ØCÚØDÚØM),(NÚD),(NÚM),А, B, М, ØN, (ØCÚØD),(ØAÚØBÚØD),(ØBÚØD),ØD, N }

5. Сформирована резольвента NÚØN= , ч.т.д.

Возможна демонстрация логического вывода с помощью графа:

(ØАÚØВÚС) (ØCÚØDÚØM) (NÚD) (NÚM) А B ØN

М

(ØCÚØD)

(ØАÚØВÚØD)

(ØВÚØD)

ØD

N



2. Доказать истинность заключения:

Решение:

1. Выполним отрицание заключения:

Ø(CÚD)=ØC&ØD

2. Формируем КНФ из посылок:

A®C=ØAÚC – элементарная дизъюнкция

B®D=ØBÚD – элементарная дизъюнкция

3. Формируем множество элементарных дизъюнкций К:

K={(AÚB), (ØAÚC), (ØBÚD), ØC, ØD},

4. Формирование резольвент:

K={(AÚB), (ØAÚC), (ØBÚD), ØC, ØD}={ (AÚB), (ØAÚC), (ØBÚD), ØC, ØD, ØA }=

{(AÚB), (ØAÚC), (ØBÚD), ØC, ØD, ØA, B }={(AÚB),(ØAÚC),(ØBÚD),ØC, ØD,ØA,B, D }

5. Сформирована резольвента DÚØD=, ч.т.д.

3. Доказать истинность заключения:

Решение:

1. Выполним отрицание заключения:

Ø(ØА&ØC)= AÚC – элементарная дизъюнкция

2. Формируем КНФ из посылок:

((AÚB)®C)=Ø(AÚB)ÚC=(ØA&ØB)ÚC=(ØAÚC)&(ØBÚC)

(C®(DÚE))=ØCÚDÚE – элементарная дизъюнкция

(E®F)=ØEÚF – элементарная дизъюнкция

(ØD&ØF) - КНФ

3. Формируем множество элементарных дизъюнкций К:

K={(AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF},

4. Формирование резольвент:

K={ (AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF}=

{(AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF, C }=

{(AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF, C, (DÚE) }=

{(AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF, C, (DÚE), E }=

{(AÚC), (ØAÚC), (ØBÚС), (ØCÚDÚE), (ØEÚF), ØD, ØF, C, (DÚE), E, F }

5. Сформирована резольвента FÚØF=, ч.т.д.

4. Доказать истинность заключения:

Решение:

1. Выполним отрицание заключения:

Ø(А&B)=ØAÚØB – элементарная дизъюнкция

2. Формируем КНФ из посылок:

(AÚB) – элементарная дизъюнкция

(А®В)=ØAÚB – элементарная дизъюнкция

(В®A)=ØВÚA – элементарная дизъюнкция

3. Формируем множество элементарных дизъюнкций К:

K={(ØAÚØВ), (AÚВ), (ØАÚВ), (ØВÚA)},

4. Формирование резольвент:

K={ (ØAÚØВ), (AÚВ), (ØАÚВ), (ØВÚA) }={(ØAÚØВ), (AÚВ), (ØАÚВ), (ØВÚA), ØВ }=

{(ØAÚØВ), (AÚВ), (ØАÚВ), (ØВÚA), ØВ, ØА }={(ØAÚØВ), (AÚВ), (ØАÚВ), (ØВÚA), ØВ, ØА, В }

5. Сформирована резольвента BÚØB=, ч.т.д.

5. Доказать истинность заключения:

Решение:

1. Выполним отрицание заключения:

Ø(А®F)=Ø(ØAÚF)=A&ØF

2. Формируем КНФ из посылок:

((AÚB)®C&D)=Ø(AÚB)ÚC&D=(ØА&ØВ)ÚС&D=

((ØА&ØВ)ÚС)&((ØА&ØВ)ÚD)=(ØАÚС)&(ØВÚС)&(ØАÚD)&(ØВÚD)

((DÚB)®F)=Ø(DÚB)ÚF=(ØD&ØB)ÚF=(ØDÚF)&(ØBÚF)

3. Формируем множество элементарных дизъюнкций К:

K={(ØAÚF), (ØAÚС), (ØBÚС), (ØАÚD), (ØBÚD), (ØDÚF), (ØBÚF)}

4. Формирование резольвент (объединяемые дизъюнкты, содержащие контрарные атомы, показаны полужирным курсивом):

K={ A, ØF, (ØAÚС), (ØBÚС), (ØАÚD), (ØBÚD), (ØDÚF), (ØBÚF)}=

{A, ØF, (ØAÚС), (ØBÚС), (ØАÚD), (ØBÚD), (ØDÚF), (ØBÚF), D }=

{A, ØF, (ØAÚС), (ØBÚС), (ØАÚD), (ØBÚD), (ØDÚF), (ØBÚF), D, F }

5. Сформирована резольвента FÚØF=, ч.т.д.

6. Доказать истинность заключения:

Решение:

1. Выполним отрицание заключения:

Ø (D«ØB)=Ø((D®ØB)&(ØB®D))=Ø(ØDÚØB)ÚØ(BÚD)= (D&B)Ú(ØB&ØD)= ((D&B)ÚØB)&((D&B)ÚØD)=(DÚØB)&(ØBÚB)&(DÚØD)&(BÚØD)=(DÚØB)&(BÚØD)

2. Формируем КНФ из посылок:

(A®B)=ØAÚB – элементарная дизъюнкция

(С®D)=ØСÚD – элементарная дизъюнкция

(AÚC) – элементарная дизъюнкция

(A®ØD)=ØAÚØD – элементарная дизъюнкция

(C®ØB)=ØСÚØB

3. Формируем множество элементарных дизъюнкций К:

K={(DÚØB), (ВÚØD), (ØАÚВ), (ØСÚD), (AÚC), (ØАÚØD), (ØCÚØB)}

4. Формирование резольвент:

K={(DÚØB), (ВÚØD), (ØАÚВ), (ØСÚD), (AÚC), (ØАÚØD), (ØCÚØB) }=

{ (DÚØB), (ВÚØD), (ØАÚВ), (ØСÚD), (AÚC), (ØАÚØD), (ØCÚØB), (ØСÚØD) }=

{(DÚØB), (ВÚØD), (ØАÚВ), (ØСÚD), (AÚC), (ØАÚØD), (ØCÚØB), (ØСÚØD), (ØСÚØВ) }=

{(DÚØB), (ВÚØD), (ØАÚВ), (ØСÚD), (AÚC), (ØАÚØD), (ØCÚØB), (ØСÚØD), (ØСÚØВ), (ØВÚА) }

5. Сформирована резольвента (ØAÚB)Ú(ØBÚA)=, ч.т.д.

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

Дата добавления: 2014-01-04