Расширение системы Prolog

Еще один способ создания средства автоматического доказательства теорем состоит в том, чтобы начать с компилятора Prolog и дополнить его в целях получения непротиворечивого и полного средства формирования рассуждений для полной логики первого порядка, Именно этот подход был принят при создании программы РТТР (Prolog Technology Theorem Prover) [1463]. Как описано ниже, программа РТТР включает пять существенных дополнений к системе Prolog, позволяющих восстановить полноту и выразительность алгоритма обратного логического вывода.

•    В процедуру унификации снова вводится проверка вхождения для того, чтобы эта процедура стала непротиворечивой.

•    Поиск в глубину заменяется поиском с итеративным углублением. Это позволяет добиться того, чтобы стратегия поиска стала полной, а увеличение продолжительности поиска измерялось лишь постоянной зависимостью от времени.

•    Разрешается применение отрицаемых литералов (таких как). В этой реализации имеется две отдельные процедуры; в одной из них предпринимается попытка доказать Р, а в другой — доказать

•    Выражение с η атомами хранится в виде η различных правил. Например, при наличии в базе знаний выражениядолжно быть также предусмотрено хранение в ней этого выражения, представленного как и как Применение такого метода, известного под названием блокирование (locking), означает, что текущая цель требует унификации только с головой каждого выражения, и вместе с тем позволяет должным образом учитывать отрицание.

• Логический вывод сделан полным (даже для нехорновских выражений) путем добавления правила резолюции с линейным входным выражением: если текущая цель унифицируется с отрицанием одной из целей в стеке, то данная цель может рассматриваться как решенная. В этом состоит один из способов рассуждения от противного. Предположим, что первоначальной целью было высказывание Ρ и что эта цель свелась в результате применения ряда этапов логического вывода к цели. Тем самым установлено, чтоа это выражение логически эквивалентно Р.

Несмотря на эти изменения, программа РТТР сохраняет свойства, благодаря которым обеспечивается высокое быстродействие системы Prolog. Операции унификации все еще осуществляются посредством непосредственной модификации переменных, а отмена связывания выполняется путем разгрузки контрольного стека во время возврата. Стратегия поиска все еще основана на резолюции с применением входных выражений, а это означает, что в каждой операции резолюции участвует одно из выражений, содержащихся в первоначальной формулировке задачи (а не какое-то производное выражение). Такой подход позволяет осуществить компиляцию всех выражений из первоначальной формулировки задачи.