ВУЗ:
Составители:
Таким образом, теорема доказана.
В настоящее время предложено множество различных стратегий метода резолю-
ций. Среди них различаются полные и неполные стратегии. Полные стратегии − это такие,
которые гарантируют нахождение доказательства теоремы, если оно вообще существует.
Неполные стратегии могут в некоторых случаях не находить доказательства, зато они ра-
ботают быстрее. Следует иметь в виду, что автоматическое доказательство теорем мето-
дом резолюций имеет по существу переборный характер, и этот перебор столь велик, что
может быть практически неосуществим за приемлемое время.
При автоматическом доказательстве теорем методом резолюций основная доля вы-
числений приходится на поиск унифицируемых дизъюнктов. Таким образом, эффективная
реализация алгоритма унификации критически важна для практической применимости
метода резолюций.
Рассмотрим следующий пример из [2], показывающий как можно получить ответы
на вопросы с помощью метода резолюций. Предположим, что у нас есть предикат F(x,y),
означающий, что «x − отец y», и истинна следующая формула
F(john,harry) & F(john,sid) & F(sid,liz).
Таким образом, у нас есть три дизъюнкта. Они не содержат переменных или импликаций,
а просто представляют базисные факты.
Введем еще три предиката M(x), S(x,y) и B(x,y), означающие соответственно, что x −
мужчина, что он единокровен с y, что он брат y. Мы можем записать следующие аксиомы
о семейных отношениях:
∀x,y (F(x,y) ⊃ M(x));
∀x,y,w ((F(x,y) & F(x,w)) ⊃ S(y,w));
∀x,y ((S(x,y) & M(x)) ⊃ B(x,y)).
Они утверждают следующее: 1) все отцы − мужчины; 2) если у детей один отец, то они
единокровны; 3) брат − это единокровный мужчина.
Пусть мы задали вопрос ∃z B(z,harry)? Чтобы найти ответ с помощью метода резо-
люции, мы записываем отрицание вопроса ∀z¬B(z,harry). Затем приводим аксиомы к
нормальной форме и записываем каждый дизъюнкт в отдельной строке (так как каждый
дизъюнкт истинен сам по себе):
1. ¬F(x,y) ∨ M(x);
2. ¬F(x,y) ∨ ¬F(x,w) ∨ S(y,w);
3. ¬S(x,y) ∨ ¬M(x) ∨ B(x,y);
4. F(john,harry);
5. F(john,sid);
6. F(sid,liz);
7. ¬B(z,harry).
Для применения резолюции необходимо найти для данной пары дизъюнктов такую
подстановку термов вместо переменных, чтобы после нее некоторый литерал одного из
дизъюнктов стал отличаться от некоторого литерала другого дизъюнкта лишь отрицани-
ем. Если, например, мы подставим john вместо x и sid вместо y, то получим следующее:
¬F(john,sid) ∨ ¬F(john,w) ∨ S(sid,w).
Мы можем применить правило резолюции к этому дизъюнкту и к (5), что дает но-
вый дизъюнкт
8. ¬F(john,w) ∨ S(sid,w) (5, 2) {x→john,y→sid}
Продолжая, получим
9. S(sid,harry) (4, 8) {w→harry}
10. M(sid) (6, 1) {x→sid,y→liz}
11. ¬S(sid,y) ∨ B(sid,y) (10, 3) {x→sid}
12. B(sid,harry) (9, 11) {y→harry}
13. (12, 7) {z→sid}
40
Страницы
- « первая
- ‹ предыдущая
- …
- 38
- 39
- 40
- 41
- 42
- …
- следующая ›
- последняя »
