Поиск доказательства в системе резолюций
В качестве примера положим, что множество Т, как и ранее, имеет вид {{ p,q},{ q, r},{p}}. Мы пытаемся показать, что Т|- r. Для этого докажем, что фраза {r} является следствием существующего множества Т, для чего добавим к этому множеству отрицание фразы r. Поиск противоречия происходит следующим образом:
- [{q,r},{r}]/{q}
- [{p,q},{q}]/{q}
- [{p},{p}]/{}
Этот метод доказательства теорем получил название "опровержение резолюции", поскольку, во-первых, он использует правило вывода резолюций, а во-вторых, следует стратегии "от противного" (стратегии опровержения).
Теперь вернемся к примеру PROLOG-программы, представленному в листинге 8.1. На рис. 8.1 показано дерево доказательства утверждения above(a, с). Дерево строится сверху вниз, и каждая ветвь связывает две "родительские фразы", в которых содержатся дополняющие литералы, с фразой, которая образуется в результате применения правила резолюции. Ко всем целям, записанным справа от значка ":-", неявно применяется отрицание. В левой части дерева представлены формулы целей, а в правой – фразы, взятые из базы данных.
Корнем дерева является пустая фраза {}. Это означает, что поиск доказательства был успешным. Добавление негативной фразы: – above (а, с) к исходному множеству (теории) привело к противоречию. Таким образом, можно утверждать, что фраза above (а, с) является логическим следствием из этой теории.
Обратите внимание на роль операции унификации в этом доказательстве. Цель above (а, с) унифицируется с головной фразой above(X, Y) с помощью подстановки {Х/а, Y/c}, где выражение Х/а можно интерпретировать как X получает значение а. Затем эта подстановка применяется к хвостовой части фразы:
on(Z, Y), above(X, Z),
Из чего следует формулировка подцелей:
on(Z, с), above(a, Z).
Следующая подцель on(Z, с) унифицируется с on(b, с) подстановкой {Z/b}. Эта подстановка затем применяется и к оставшейся подцели, которая таким образом превращается в above (а, b), и так до тех пор, пока не образуется пустая фраза.
Рис. 8.1. Дерево доказательства методом опровержения резолюций
Восходящий процесс доказательства, использующий в качестве отправной точки утверждение, которое мы стараемся доказать, позволяет сфокусировать внимание на процессе поиска решения, поскольку анализируемые логические связи по крайней мере потенциально ведут нас к цели. Правда, основанный на этой стратегии метод опровержения резолюций не позволяет решить все перечисленные выше проблемы. В частности, этот метод не гарантирует, что найденный путь доказательства будет короче других (или длиннее).
В следующих двух разделах мы рассмотрим эволюцию процедурных дедуктивных систем, т.е. систем, в которых процедуры используются для добавления дополнительных управляющих свойств в процесс целенаправленного поиска и для представления знаний, которые не имеют четко выраженного декларативного характера.
Процесс становления этого класса систем весьма поучителен, поскольку демонстрирует, как, отталкиваясь от стандартной логики и добавляя методики, обычно используемые при доказательстве теорем, можно построить успешно функционирующую автоматическую систему доказательства.