ВУЗ:
Составители:
1. Среди текущего множества дизъюнктов нет резольвируемых. Это означает, что
множество формул Γ выполнимо.
2. В результате очередного применения правила резолюции получен пустой дизъ-
юнкт. Это означает, что множество формул Γ невыполнимо
3. Процесс не заканчивается, то есть множество дизъюнктов пополняется все но-
выми резольвентами, среди которых нет пустых. Выполнение алгоритма не завершится,
например, для множества {P, ¬P ∨ Q}. Резольвентный дизъюнкт Q будет порождаться не-
ограниченное число раз.
Алгоритм проверки невыполнимости − недетерминированный: вообще говоря,
возможен не один выбор для резольвируемых дизъюнктов и контрарных литералов. В
приведенном примере мы выбирали дизъюнкты C и D в лексикографическом порядке но-
меров. Такая стратегия неоптимальная. Некоторые резольвенты оказались ненужными, а
также вычислялись в некоторых случаях более одного раза. Для сравнения продемонстри-
руем теперь применение этого же алгоритма с минимумом резолюций:
5. Q (1, 4)
6. R (2, 4)
7. ¬Q (3, 6)
8. (5, 7)
Конкретные реализации выбора резольвируемых дизъюнктов и контрарных лите-
ралов называются стратегиями метода резолюции.
6.10 Опровержение методом резолюций
Опровержение методом резолюций − это алгоритм автоматического доказательства
теорем в прикладном исчислении предикатов, который сводится к следующему. Пусть
нужно установить выводимость Γ |− G.
Каждая формула множества Γ и формула ¬G (отрицание целевой теоремы) незави-
симо преобразуется во множества дизъюнктов. Пусть C
−
полученное совокупное множе-
ство дизъюнктов.
Теорема 13. Множество дизъюнктов C невыполнимо тогда и только тогда, когда Γ |− G.
С помощью алгоритма резолюций, примененному к множеству дизъюнктов C, мы
можем установить выводимость Γ |− G.
При работе алгоритма возможны три случая.
1. На каком-то этапе отсутствуют резольвируемые дизъюнкты. Это означает, что
теорема опровергнута, то есть формула G не выводима из множества формул Γ.
2. В результате очередного применения правила резолюции получен пустой дизъ-
юнкт. Это означает, что теорема доказано, то есть Γ |− G.
3. Процесс не заканчивается, то есть множество дизъюнктов пополняется все но-
выми резольвентами, среди которых нет пустых. Это ничего не означает.
Замечание. Таким образом, исчисление предикатов является полуразрешимой тео-
рией, а метод резолюций является частичным алгоритмом автоматического доказательст-
ва теорем.
Пример. Докажем методом резолюций теорему |− (((A ⊃ B) ⊃ A) ⊃ A). Сначала
нужно преобразовать в дизъюнкты отрицание целевой формулы ¬(((A ⊃ B) ⊃ A) ⊃ A). Ис-
пользуя правила из пункта «Сведения к дизъюнктам», получаем множество дизъюнктов
{A∨A, ¬B∨A, ¬A}.
После этого проводится резольвирование имеющихся предложений 1−3.
1. A∨A.
2. ¬B∨A.
3. ¬A.
4. A (1, 3)
5. (3, 4).
39
Страницы
- « первая
- ‹ предыдущая
- …
- 37
- 38
- 39
- 40
- 41
- …
- следующая ›
- последняя »
