Для иллюстрации работы алгоритма FOL-FC-Ask воспользуемся описанной выше задачей доказательства преступления. Импликационными высказываниями являются высказывания, приведенные в уравнениях 9.3, 9.6-9.8. Требуются следующие две итерации.

•    В первой итерации правило 9.3 имеет невыполненные предпосылки.

Правило 9.6 выполняется с подстановкой {x/Μ1} и добавляется высказывание Sells (West, M1, Nono).

Правило 9.7 выполняется с подстановкой {х/М1} и добавляется высказывание Weapon (M1) .

Правило 9.8 выполняется с подстановкой {x/Nono} и добавляется высказывание Hostile(Nono).

•    На второй итерации правило 9.3 выполняется с подстановкой [x/West, y/M1, z/Nono] и добавляется высказывание Criminal (West).

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

Рис. 9.2. Дерево доказательства, сформированное путем прямого логического вывода в примере доказательства преступления. Первоначальные факты показаны на нижнем уровне, факты, выведенные логическим путем в первой итерации, — на среднем уровне, а факт, логически выведенный во второй итерации, — на верхнем уровне