МАТ_ ЛОГИКА / МАТЕМАТИЧЕСКАЯ ЛОГИКА_ЛК9_12_03_2012_Метод резолюций (для высказываний)__
.docМетод резолюции
Существует эффективный алгоритм логического вывода - принцип (или метод) резолюции Дж. Робинсона. Он показал, что выводимость формулы В из множества посылок и аксиом F1 F2, F3, ..., Fn равносильна доказательству теоремы:
|— (F1F2F3. . . FnB),
|— ((F1F2F3. . . Fn)B),
Из того, что ((F1F2F3. . . Fn)B)=И следует, что
(F1F2F3...Fn (B))=Л.
Так как (F1F2F3...Fn (B)) есть КНФ, то все Fi и B должны быть приведены к КНФ. Множество элементарных дизъюнктов (входящих в КНФ): К={D1, D2, ..., Dm}. Два дизъюнкта Di и Dj , содержащие одинаковые пропозициональные переменные, но с противоположными знаками, объединяют в третий дизъюнкт Dk=(DiDj) – резольвенту, из которой удаляются эти переменные. Пропозициональные переменные с противоположными знаками называют контрарными атомами. Если Di=А, Dj=A, то Dk=(DiDj)=(АA) есть пустая резольвента, которую обозначают символом . Многократно применяя процедуру объединения дизъюнктов множества К с контрарными атомами стремятся получить пустую резольвенту. Наличие пустой резольвенты означает, что выводима формула
|— ((F1F2F3. . . Fn)B).
Алгоритм вывода по методу резолюции:
Шаг 1: принять отрицание заключения, т.е. В,
Шаг 2: привести все формулы посылок и отрицания заключения в конъюнктивную нормальную форму,
Шаг 3: выписать множество дизъюнктов всех посылок и отрицания заключения: К = {D1 D2, ..., Dk },
Шаг 4: выполнить анализ пар множества К по правилу: «если существуют дизъюнкты Di и Dj, один из которых (Di) содержит атом А, а другой (Dj) - атом А, то соединить эту пару логической связкой дизъюнкции (DiDj) и сформировать новый дизъюнкт - резольвенту, исключив контрарные атомы А и А, а резольвенту включить в множество К»,
Шаг 5: если в результате соединения дизъюнктов получена пустая резольвента (пустой дизъюнкт), то конец (доказательство подтвердило истинность заключения), иначе включить резольвенту в множество дизъюнктов К и перейти к шагу 4 (по закону идемпотентности любой дизъюнкт и любую резольвенту можно использовать неоднократно, т.е. из множества К не следует удалять использованные в соединении дизъюнкты).
Многие правила (modus ponens, транзитивность и др.) – частные проявления правила резолюции. В таблице слева приведены названия, в центре – традиционные формы известных правил вывода, справа – те же самые правила, записанные в обозначениях метода резолюции.
Название правила |
Традиционная форма |
Резолютивная форма |
Modus ponens |
||
Транзитивность |
||
Слияние |
Пример Доказать истинность заключения для правила Modus ponens
по методу резолюции.
Вывод по методу резолюции:
А – первая посылка содержит один дизъюнкт,
- вторая посылка содержит один дизъюнкт,
¬В - отрицание заключения содержит один дизъюнкт.
Множество дизъюнктов:
K={А, (AB), В}.
(AB) В≡A – резольвента.
Множество дизъюнктов:
K1={А, (AB), В, A}.
AА≡ - пустая резольвента.
Пример Доказать истинность заключения для правила
по методу резолюции.
Вывод по методу резолюции:
- первая посылка содержит один дизъюнкт,
- вторая посылка содержит один дизъюнкт,
- отрицание заключения содержит два дизъюнкта А и ¬С.
Множество дизъюнктов:
K={(AB), (ВС), А, С}.
(AB) (ВС )≡(AС) – резольвента.
Множество дизъюнктов:
K1={(AB), (ВС), А, С, (AС)}.
С(AС) ≡A – резольвента.
Множество дизъюнктов:
K2={(AB), (ВС), А, С, (AС), A}.
AА≡ - пустая резольвента.
Пример Доказать истинность заключения по методу резолюции: (ABC),(CD M), (NDM)
(ABN)
Вывод по методу резолюции:
ABC ( AB)C (ABC) – первая посылка содержит один дизъюнкт,
CDM (CD)M (CDM) – вторая посылка содержит один дизъюнкт,
NDM NDM (ND) (NM) – третья посылка содержит два дизъюнкта,
((AB) N) ABN - отрицание заключения содержит три однолитерных дизъюнкта,
Множество дизъюнктов:
K={(ABC), (CDM), (ND), (NM), А, В, N},
(MN)N М - резольвента,
Множество дизъюнктов:
K1={(ABC), (CDM), (ND), (NM), А, В, N, М},
(CDM)M (CD) - резольвента,
Множество дизъюнктов:
K2={(ABC), (CDM), (ND), (NM), А, В, N, М, (CD)},
(¬A¬BC) (¬C¬D) (¬A¬B¬D) - резольвента,
Множество дизъюнктов:
K3={(ABC), (CDM), (ND), (NM), А, В, N, М, (CD), (¬A¬B¬D)},
(¬A¬B¬D) A (¬B¬D) - резольвента,
Множество дизъюнктов:
K4={(ABC), (CDM), (ND), (NM), А, В, N, М, (CD), (¬A¬B¬D), (¬B¬D)},
(¬B¬D)B ¬D - резольвента,
Множество дизъюнктов:
K5={(ABC), (CDM), (ND), (NM), А, В, N, М, (CD), (¬A¬B¬D), (¬B¬D), D},
D (ND) N - резольвента,
Множество дизъюнктов:
K6={(ABC), (CDM), (ND), (NM), А, В, N, М, (CD), (¬A¬B¬D), (¬B¬D), D, N},
NN - пустая резольвента, что и требовалось доказать.
Рис. 1. Граф вывода (ABN) по принципу резолюции.
Для демонстрации удобно использовать граф типа дерево, корнем которого является один из дизъюнктов отрицания заключения, а листьями- дизъюнкты всех посылок и отрицания заключения. Тогда узлами графа являются резольвенты. На рис. 1. показан граф вывода этой задачи.
Пример Доказать истинность заключения:
(А В) (С D), (D В М), М
(AC)
Вывод по методу резолюции:
(AB) (CD) (AB) (CD) - посылка,
DBM (DB)M (DBM) - посылка,
M - посылка,
(AC ) = AC - отрицание заключения,
Множество дизъюнктов:
К ={А, С, М, (AB), (CD), (DBM)},
A (AB) В - резольвента,
Множество дизъюнктов:
К1 ={А, С, М, (AB), (CD), (DBM), В},
B(DBM) (DM) - резольвента,
Множество дизъюнктов:
К2 ={А, С, М, (AB), (CD), (DBM), В, (DM)},
(DM) (CD) (CM) - резольвента,
Множество дизъюнктов:
К3 ={А, С, М, (AB), (CD), (DBM), В, (DM), (CM)},
(CM) M C - резольвента,
CC - пустая резольвента, ч.т.д.
На рис. 2 показан граф вывода этой задачи.
Рис.2. Граф вывода (AC) по принципу резолюции.
Пример. Работа автоматического устройства, имеющего три клапана А, В и С, удовлетворяет следующим условиям: если не срабатывают клапаны А или В или оба вместе, то срабатывает клапан С; если срабатывают клапаны А или В или оба вместе, то не срабатывает клапан С. Следовательно, если срабатывает клапан С, то не срабатывает клапан В.
Доказать истинность заключения:
((¬А¬В¬АВ) С), ((АВАВ) С)
(С В)
Вывод по методу резолюции:
(¬А¬B¬А¬B) С (¬А(¬B¬А)¬B) С =
= ¬ (¬А(¬B¬А)¬B) С=¬¬А¬ ((¬B¬А)¬B)) С=
=А ( ¬ (¬B¬А) ¬¬B))С=А((BА)B))С=АBС=(АC)(BC) – первая посылка, содержит два дизъюнкта: (АC) и (BC);
(ABАB) ¬ C (АC) (BC) – вторая посылка, содержит два дизъюнкта:
(АC) и (BC);
¬(CВ)=¬(¬CВ)=¬¬C¬¬В=CВ - отрицание заключения, содержит два дизъюнкта: С и В.
Множество дизъюнктов:
K={(АC), (BC), (АC), (BC), С, В}.
С(ВC) = В - резольвента,
множество дизъюнктов:
K1={(АC), (BC), (АC), (BC), С, В, В},
ВВ = - пустая резольвента.
Доказано, что если срабатывает клапан С, то не срабатывает клапан В.
Пример. Доказать истинность заключения
A; В; (СAB)
С.
1) A - посылка;
2) B - посылка;
3) CA B = (CAB) - посылка;
4) (C) = C - отрицание заключения;
5) множество дизъюнктов: K={A; B; (CAB); C};
6) A(CAB)=(СB) - резольвента из 1) и 3);
7) K1={A; B; (CAB); C; (СB)};
8) B(СB)=C - резольвента из 2) и 6);
9) K2={A; B; (CAB); C; (СB); C };
10) СC = - пустая резольвента из 4) и 7).
1)-10) - доказательство истинности заключения C по принципу резолюции.
Пример. Доказать истинность заключения
(AB)(CD); (DBM);¬ M
(¬A¬C)
1) (AB)(CD)=( ¬AB)( ¬CD) - посылка;
2) DBM=¬ (DB)M=(¬D¬BM) - посылка;
3) ¬ M - посылка;
4) ¬( ¬ A ¬ C ) = A C - отрицание заключения;
5) K ={A; C; ¬M; (¬AB); (¬CD); (¬D¬BM)}
6) A(¬AB)=B - резольвента;
7) B(¬D¬BM)=( ¬DM) - резольвента;
8) (¬DM)( ¬CD)=( ¬CM) - резольвента;
9) (¬CM) ¬M=¬C - резольвента; 10) ¬CC= - пустая резольвента.
1)-10) - доказательство истинности заключения (¬A¬C).
Достоинством принципа резолюции является то, что при доказательстве применяют только одно правило: поиск и удаление контрарных атомов дизъюнктов, а для этого механизм вывода использует правила подстановки и унификации дизъюнктов.