Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Логическое программирование
Логическое программирование

•    В языке Prolog допускается определенная форма отрицания —отрицание как недостижение цели. Отрицаемая цель not P считается доказанной, если системе не удается доказать Р. Таким образом, следующее высказывание:

можно прочитать так: "Любого следует считать живым, если нельзя доказать, что он мертв".

•    В языке Prolog предусмотрен оператор равенства, "=", но он не обладает всей мощью логического равенства. Цель с оператором равенства достигается успешно, если в ней два терма являются унифицируемыми, а в противном случае попытка ее достижения оканчивается неудачей. Таким образом, цель x+Y=2+3 достигается успешно, после связывания переменной X со значением 2, a Y — со значением 3, а попытка достижения цели morningstar=evenings tar оканчивается неудачей. (В классической логике последнее равенство может быть или не быть истинным.) Не могут быть подтверждены (введены в базу знаний) какие-либо факты или правила, касающиеся равенства.

•    Из алгоритма унификации Prolog исключена проверка вхождения. Это означает, что могут быть сделаны некоторые противоречивые логические выводы; такая проблема возникает редко, за исключением тех ситуаций, когда язык Prolog используется для доказательства математических теорем.

Решения, принятые при проектировании языка Prolog, представляют собой компромисс между стремлениями обеспечить декларативность и вычислительную эффективность (по крайней мере, эффективность в той ее трактовке, которая существовала в период разработки языка Prolog). Мы вернемся к этой теме после рассмотрения того, как реализована система Prolog.