Основы современных компьютерных технологий


Пролог и логическое программирование - часть 3


Все переменные в предложениях связаны квантором общности, поэтому обычно знак квантора ? опускается.

Формула с использованием связок > и ? может быть преобразована в эквивалентную, но имеющую связки ¬ (HE) и ? (ИЛИ), формулу вида:

A0? ¬A1? ¬A2?... ? ¬Am(m ? 0).

Такие формулы и называются хорновскими дизъюнктами, а стиль программирования - хорновским.

Процедурная интерпретация правил Пролога вида:

А0:-А1, А2... Аm или А0 if А1 and A2 and ... and Am

следующая: "для достижения цели А0 необходимо последовательно достичь целей А1 , А2 . . . Am"

Соответственно, для фактов (когда m = 0) имеет место логическое прочтение: "А0 истинно", процедурная интерпретация факта: "цель А достигнута".

Логическая семантика запроса G: С1,С2...Сr(с переменными x1,х2...хi) к логической программе понимается как требование вычислить все значения переменных x1,х2...хi, при которых утверждение С1 ? С2 ?... ? Сr логически следует из утверждений программы или, записывая это, как принято в логике, необходимо показать, что

? G

305

т.е. запрос G логически следует (выводим) из логической программы . При этом оказывается, что доказательство выводимости G из аналогично тому, чтобы показать

, ¬ G ?

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

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

Унификация - процесс, на вход которого поступает два терма и для них находится унификатор. Унификатором двух термов называется подстановка, которая делает термы одинаковыми.


Начало  Назад  Вперед



Книжный магазин