Структуры данных и модели вычислений
в сколемовской формуле используются только
Поскольку в сколемовской формуле используются только кванторы общности и все они расположены в начале формулы, их обычно опускают, подразумевая по умолчанию их наличие, а бескванторную часть представляют в нормальной конъюнктивной форме. Полученная таким образом формула называется клаузальной. В нашем случае формула (2) превращается в клаузальную формулу
(3) |
Упомянутый выше метод резолюций основывается на единственном правиле вывода, называемом правилом резолюции, которое заключается в следующем. Из двух формул вида
и
в соответствии с правилом резолюции выводится формула
Видно, что клаузальная форма хорошо приспособлена для применения правила резолюции. Детали этого применения в логике предикатов будут рассмотрены ниже.
Из математической логики известно, что не существует алгоритма, который по любому множеству формул-гипотез логики предикатов и еще одной формуле отвечал бы на вопрос, является ли
логическим следствием множества . Однако существует алгоритм, который в случае, когда логически следует из , строит доказательство этого факта с использованием правила резолюции, в противном случае алгоритм может работать бесконечно.
Различные версии языка Пролог базируются на использовании так называемых хорновских клаузальных формул. Хорновскими называются формулы, являющиеся дизъюнкциями атомарных формул и/или их отрицаний, причем атомарная часть без отрицания может быть в такой формуле не более чем одна. Рассмотрим пример такой формулы:
(4) |
Ее можно представить в виде
(5) |
Эта формула воспринимается Прологом так, как если бы все ее переменные были связаны квантором общности. Восстанавливая кванторы, имеем
(6) |
Учитывая, что не входит в правую часть импликации, формулу (6) можно переписать в виде
изменив область действия квантора .
В Прологе принято формулы, аналогичные формуле (5), записывать в виде
(7) |
меняя местами левую и правую части импликации и вместо знака конъюнкции ставя запятую.
Формулу (7) Пролог воспримет как указание на то, что для доказательства истинности надо найти некоторое значение
и доказать, что истинны , , . Такие формулы принято называть правилами.
Если в хорновской клаузальной формуле отсутствуют атомарные части с отрицанием, то такая формула называется фактом. Если в хорновской клаузальной формуле отсутствует атомарная часть без отрицания, то такая формула называется запросом. Программой в Прологе называется набор фактов и правил.
По заданной программе и запросу система Пролог определяет, является ли запрос логическим следствием фактов и правил программы. При этом если в запросе имеются свободные переменные, то в процессе поиска доказательства эти переменные конкретизируются, то есть принимают конкретные значения, и при успешном его завершении эти конкретизированные значения являются ответом к поставленной задаче. Если же доказательство не будет найдено, то система ответит "no".
