(5) Преобразование в префиксную форму. На этом шаге все оставшиеся кванторы (останутся только кванторы общности) переносятся "в голову" выражения и таким образом оказываются слева в списке квантифицированных переменных. За ними следует матрица, в которой отсутствуют кванторы.

(6) Разнести операторы дизъюнкции и конъюнкции.

(7) Отбросить кванторы общности. Теперь все свободные переменные являются неявно универсально квантифицированными переменными. Экзистенциальные переменные станут либо константами, либо функциями универсальных переменных.

(8) Как и ранее, отбросить операторы конъюнкций, оставив множество фраз.

(9) Снова переименовать переменные, чтобы одни и те же имена не встречались в разных фразах.

Исчисление предикатов в упрощенном виде. Там выражение вида

at(робот, комнатаА)

означает, что робот находится в комнате А. Термы робот и комнатаА в этом выражении представляли собой константы, которые описывали определенные реальные объекты. Но что будет означать выражение вида

at(X, комнатаА) ,

в котором х является переменной? Означает ли оно, что нечто находится в комнате А? Если это так, то говорят, что переменная имеет экзистенциальную подстановку (импорт). А может быть, выражение означает, что все объекты находятся в комнате А? В таком случае переменная имеет универсальную подстановку. Таким образом, отсутствие набора четких правил не позволяет однозначно интерпретировать приведенную формулу.

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

В частности, фраза

at(X, комнатаА )<—at (X, ящик1) интерпретируется как

"для всех X X находится в комнате А, если X находится в ящике 1". В этой фразе переменная имеет универсальную подстановку. Аналогично, фраза

at(X, комнатаА) <-интерпретируется как "для всех X X находится в комнате А". А вот фраза

<— at(X, комнатаА) интерпретируется как "для всех XX не находится в комнате А".

Иными словами, это не тот случай, когда некоторый объект X находится в комнате А и, следовательно, переменная имеет экзистенциальную подстановку.

Теперь можно преобразовать фразовую форму, в которой позитивные литералы сгруппированы слева от знака стрелки, а негативные — справа. Если фраза в форме

P1, ..., Рт <— q1,...qn содержит переменные х1,..., хk, то правильная интерпретация имеет следующий вид:

для всех x1, ..., хk

p1 или ... или pm является истинным, если q1 и ... и qn являются истинными.

Если п = 0, т.е. отсутствует хотя бы одно условие, то выражение будет интерпретироваться следующим образом:

для всех x1, ..., xk

p1 или ... или рт является истинным.

Если т = 0, т.е. отсутствуют термы заключения, то выражение будет интерпретироваться следующим образом:

для всех x1, ..., xk

не имеет значения, что q1 и ... и qn являются истинными.

Если же т = п = 0, то мы имеем дело с пустой фразой, которая всегда интерпретируется как ложная.

3.2 Программирование на ПРОЛОГЕ.

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

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

В Прологе очень компактно, по сравнению с императивными языками, описываются многие алгоритмы. По статистике, строка исходного текста программы на языке Пролог соответствует четырнадцати строкам исходного текста программы на императивном языке, решающем ту же задачу. Пролог-программу, как правило, очень легко писать, понимать и отлаживать. Это приводит к тому, что время разработки приложения на языке Пролог во многих случаях на порядок быстрее, чем на императивных языках. В Прологе легко описывать и обрабатывать сложные структуры данных.

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

Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна представляется выражением

В языке PROLOG эта же фраза записывается в таком виде:

р :- q1,...,qn. Такая фраза интерпретируется следующим образом:

"Для всех значений переменных в фразе p истинно, если истинны q1 и ... и qn",

т.е. пара символов ":-" читается как "если", а запятые читаются как "и".

PROLOG — это не совсем обычный язык программирования, в котором программа состоит в основном из логических формул, а процесс выполнения программы представляет собой доказательство теоремы определенного вида.

Фраза в форме

р :- q1, ...,qn.

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

(1) Литерал цели сопоставляется с литералом р (унифицируется с р), который называется головой фразы.

(2)Хвост фразы ql, ...,qn конкретизируется подстановкой значений переменных (или унификаторов), сформированных в результате этого сопоставления.

(3) Конкретизированные термы хвостовой части образуют затем множество подцелей, которые могут быть использованы другими процедурами.

Таким образом, сопоставление (или унификация) играет ту же роль, что и передача параметров функции в других, более привычных языках программирования.

Например, рассмотрим набор фраз языка PROLOG, представленных в листинге 1. Предположим, что a, b и с — какие-то блоки в мире блоков. Две первые фразы утверждают, что а находится на (on) b, a b находится на (on) с. Третья фраза утверждает, что X находится выше (above) Y, если X находится на (on) Y. Четвертая фраза утверждает, что X находится выше (above) Y, если существует какой-то другой блок Z, размещенный на (on) Y, и X находится выше (above) Y.

Листинг 1. Простая программа на языке PROLOG, определяющая отношение

on (на)

on(а, b).

on(b, с).

above(X, Y) :- on(X, Y).

above(X, Y) :- on(Z, Y),

above(X, Z).

Очевидно, что от программы требуется вывести цель above (а, с) из этого множества фраз. Процесс формулировки выражения цели включает обработку двух процедур above и использование двух фраз on. В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation).

3.3 Принцип резолюций

Мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).

Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ — пропозициональные переменные, как и раньше.

Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и

U={ U1, ..., Ui, ...., Um},

и

ф= {ф1..., фi.....,фn}, и

Ui, = ¬фi при 1[i[mm,1 [j [ n,

то новую фразу £ можно вывести из объединения U' и ф', где

U' = U¬{ Ui} и ф' = ф¬{ф,}.

Фраза £ = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и фj.

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

В левой колонке табл. 1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции:

Таблица 1. Обобщение резолюции.