Алгоритм доказательства

Пусть заданы:

 

 

Предикаты  делаются дополнительными с помощью подстановки [a/x]. Суждение о том, становятся ли два выражения дополнительными, выносится:

1. По различию используемых символов.

2. По существованию НОУ для двух выражений, в которых удалены одинаковые символы.

Далее все делается рекуррентно.

Пример 1. Милиция разыскивает всех въехавших в страну, за исключением дипломатов. Шпион въехал в страну. Однако, распознать шпиона может только шпион. Дипломат не является шпионом.

Оценим вывод: среди милиционеров есть шпион.

Воспользуемся следующими предикатами:

Въехал(x): x въехал в страну.

Дипломат(x): x – дипломат.

Поиск(x, y): x разыскивает y.

Милиционер(x): x – милиционер.

Шпион(x): x – шпион.

Если выразим через эти предикаты посылку и вывод в форме ППФ, то получим:

для всех x, если x не является дипломатом, но въехал в страну, найдется милиционер y, который его разыскивает.

Если существует шпион x, который въехал в страну, и некоторый y разыскивает его, то он сам шпион.

Для всех x справедливо, что если x является шпионом, то он не дипломат.

Заключение:

Существует x такой, что он является шпионом и милиционером.

Если эти формулы преобразовать в клаузальную нормальную форму, то получим:

 

Заключение преобразуем в свое отрицание:

 

 

и затем в клаузальную форму без квантора общности.

Последующий процесс доказательства имеет вид:

 

дипломат(а)Úмилиционер(f(а)) [a/x] из 2,4 (9)

милиционер(f(а)) [a/x] из 8,9 (10)

дипломат(а)Úпоиск(f(а),а) [a/x] из 1,4 (11)

поиск(f(а),а) [a/x] из 8,11 (12)

шпион(f(a)) [a/x] из 12,5 (13)

ð            [f(a)/x)] из 10 и 14   (15)

 

Еще одной возможностью метода резолюции является возможность получать конкретные значения переменных, содержащихся в заключении.

4.2.3.3 Задачи, использующие равенства

Новые предложения получались до сих пор двумя способами: подстановкой и резолюцией. При резолюции пары предложений, отображаются в новые предложения, а подстановка заменяет терм в предложении другим термом той же синтаксической формы. Иногда возникает необходимость заменить терм равным ему термом, который не является термом, для которого возможна подстановка (подстановочным случаем) в первом терме. Рассмотрим простой пример. Положим f(x, y) = x + y. При сравнении предложений:

 

 

у нас нет способа обнаружить противоречие, поскольку резолюция не допускает замены термов разных синтаксических форм. Поэтому имеет смысл, включить в программу, использующую принцип резолюции, специальные правило вывода, которое должно применяться, когда возникает необходимость в операции равенства. Чтобы это правило было совместимо с остальной частью программы, оно должно удовлетворять двум условиям:

1. Работать с предложениями, в которых равенство выражено в виде атомов.

2. Быть операцией, превращающей два предложения в третье.

Это специальное правило вывода называется парамодуляцией.

Пусть A, B и т.д. будут множествами литералов, а a, b, g - термами, то есть константами, переменными или функциональными выражениями. В дополнении к обычному определению атомов и литералов будем записывать атомы равенства в виде a=b (терм a равен терму b). К таким термам можно применять подстановку.