Практика по методу резолюции
Метод резолюции
Приведенные схемы дедуктивного вывода неудобны для автоматизации, поскольку требуют либо сознательного подбора соответствующих правил преобразования и подходящих формул на каждом шаге вывода, либо перебора множества формул.
Дж. Робинсон показал, что выводимость формулы Ф из множества посылок и аксиом А, В, С, … равносильна доказательству теоремы: (А&В&С&…ØФ)=л. Покажем обоснованность такого предположения:
1) Запишем формулу связи импликации и выводимости логической формулы:
|- (А&В&С&…®Ф)
2) Избавимся от импликации:
|- (Ø(А&В&С&…)ÚФ)
3) Применим закон де Моргана:
|- Ø (А&В&С&…&ØФ)
4) Поскольку данная формула выводима (знак |-), верна формула
Ø (А&В&С&…&ØФ)=и,
следовательно, (А&B&C&…&ØФ)=л.
Для определения истинности данной формулы достаточно показать ложность одной из подформул ее левой части. С этой целью Робинсон предложил эффективный алгоритм – принцип, или метод, резолюции.
Назовем два дизъюнкта, содержащие одинаковые ПП, но с противоположными знаками, контрарными атомами.
Алгоритм вывода по методу резолюции (при имеющемся заключении):
Шаг 1: принять отрицание заключения, т.е. ¬Ф,
Шаг 2: привести все формулы посылок и отрицания заключения в КНФ,
Шаг 3: сформировать множество К дизъюнктов всех посылок и отрицания заключения: K = {D1, D2, …, Dk},
Шаг 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)=, ч.т.д.
Особенностью метода резольвент является то, что для его использования должно быть известно заключение. Это ограничивает его применение и делает более универсальным метод дедукции.