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

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

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

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

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

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

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

on(а, b).

On(b, с).

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

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

Above(X, Z).

Очевидно, что от программы требуется вывести цель above (а, с) из этого множества фраз. Как это делается, мы увидим в разделе 8.3.2, но уже сейчас можно сказать, что процесс формулировки выражения цели включает обработку двух процедур above и использование двух фраз on.

Опровержение резолюций

В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation). Полное описание этого метода читатель найдет в книге Робинсона [Robinson, 1979], а в этом разделе мы попытаемся кратко изложить только основные идеи.

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

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

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

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

U={ U₁,..., Ui,...., U_m},

и

ф= {ф₁..., фi.....,ф_n}, и

U_i, = ф_i при 1[i[m m,1 [j [ n,

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

U' = U{ U_i} и ф' = ф{ф,}.

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

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

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

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

	Правило вывода	Обычная форма	Конъюнктивная нормальная форма
	Modus ponens	(U ф,U)/Ф	{U,Ф},{U}/{ф}
	Modus fallens	(U ф.ф)/-U	{U,ф},{-,ф}/{-U}
	Сцепление	(U ф,ф £)(U £)	{U,ф},{ф,£}/{U,£}
	Слияние	(U ф,U ф)/ф	{U,ф},{U,ф}/{ф}
	Reductio	(U,U)/ |	{U},{U}/{}

Обратите внимание на то, что противоречие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.

Главное, что нужно вынести из всего сказанного выше, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.

В исчислении предикатов использование резолюций требует дополнительных усилий, поскольку в этом исчислении присутствуют переменные. Основная операция сопоставления в доказательстве теорем с помощью резолюций называется унификацией (подробное описание используемого при этом алгоритма читатель найдет, например, в работе Нильсона [Nilsson, 1980]). При сопоставлении дополняющих литералов отыскивается такая подстановка переменных, которая превращает оба выражения в идентичные.

Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.