Язык программирования Пролог был разработан коллективом во главе с Колмерауэром приблизительно в 1970 году. Это была первая попытка в разработке языка, который позволял бы программисту описывать свои задачи средствами математической логики, а не с помощью традиционных для программирования конструкций, указывающих что и когда должна делать вычислительная машина. Эта идея нашла отражение в названии языка программирования «Пролог» (английское название «Prolog» является сокращением для Programming in Logic.- Перев.).

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

Если мы намерены обсуждать связь Пролога с математической логикой, то прежде всего необходимо установить, что мы понимаем под логикой. Первоначально логика развивалась как некоторый способ представления определенного класса высказываний, так чтобы можно было, используя формальную процедуру, проверить, справедливы они или нет. Таким образом, логика может быть использована для выражения высказываний, отношений между высказываниями и правил вывода одних высказываний из других. Логическое исчисление специального вида, о котором будет идти речь в этой главе, называется исчисление предикатов. Здесь мы лишь затронем некоторые вопросы исчисления предикатов. Хорошим введением в математическую логику является книга Hodges W. Logic, Penguin Books, 1977. Более подробное обсуждение предмета дано в книге Mendelson E. Intro ductiontoMathematicalLogic, VanNostrandReinhold.[15] Вы так же можете обратиться к любой книге по математической логике. Другая книга, представляющая интерес, написана Chin L. С, Lee R. С.-Т. Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.^[16]

Для того чтобы делать высказывания о мире, необходимо уметь описывать объекты этого мира. В исчислении предикатов объекты представляются с помощью термов. Существуют термы трех типов:

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

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

• Составной терм. Составной терм состоит из функционального символа и упорядоченного множества термов, являющихся его аргументами. Идея состоит в том, что составной терм обозначает тот или иной индивидуальный объект, зависящий от других индивидуальных объектов, представленных его аргументами. Функциональный символ описывает характер зависимости. Например, можно было бы иметь функциональный символ, обозначающий «расстояние» и имеющий два аргумента. В этом случае составной терм обозначает расстояние между объектами, представленными его аргументами. Составной терм можно рассматривать как структуру языка Пролог, имеющую в качестве функтора функциональный символ. Составные термы будут записываться по правилам синтаксиса Пролога так, что, например, жена(генри) может обозначать жену Генри, расстояние(точка1, X) может обозначать расстояние между некоторой заданной точкой и каким-то другим объектом, который будет указан, а классы(мэри, на_следующий_ день_после(Х)) может обозначать классы, в которых преподавала Мэри на следующий после X (необходимо указать день).

Таким образом, способы, используемые для представления объектов в исчислении предикатов, в точности соответствуют способам, имеющимся для этого в Прологе.

Для того чтобы делать высказывания об объектах, необходимо иметь возможность описывать отношения между объектами. Это делается с помощью предикатов. Атомарное высказывание (атомарная формула) состоит из предикатного символа и соответствующего ему упорядоченного множества термов, являющихся его аргументами. Это полностью аналогично целевому утверждению Пролога. Так, например, человек(мэри), владеет(Х,осел(Х)) и нравится (Мужчина, вино) являются атомарными высказываниями (атомарными формулами). В языке Пролог структура может быть использована как в качестве целевого утверждения, так и в качестве аргумента для другой структуры. В исчислении предикатов дело обстоит иначе. Там имеется строгое разделение между функциональными символами, используемыми в качестве функторов для построения аргументов, и предикатными символами, используемыми в качестве функторов для построения высказываний (формул).

Используя атомарные высказывания, можно различными способами создавать составные высказывания. Именно здесь начинают появляться понятия не имеющие непосредственных аналогов в языке Пролог. Существует несколько способов построения более сложных высказываний из более простых. Прежде всего, можно использовать логические связки. Таким способом можно выразить понятия 'не', 'и', 'или', 'влечет' и 'является эквивалентным'. Далее приведено краткое описание этих связок и вкладываемых в них значений. Здесь ? и ? используются для обозначения произвольных высказываний (формул). В следующей таблице приводятся традиционная форма записи высказываний, используемая в исчислении предикатов, и форма записи, используемая в этой главе.

Так, например, конструкция

мужчина(фред) # женщина (фред)

могла бы быть использована для представления высказывания о том, что Фред является мужчиной или Фред является женщиной. Конструкция

мужчина(джон) -› человек (джон)

могла бы представлять высказывание: то, что Джон является мужчиной, влечет то, что он является человеком (если Джон мужчина, то он – человек). Понятия импликации и эквивалентности иногда при первом знакомстве с ними представляются несколько сложными. Мы говорим, что α влечет β, если всякий раз, когда α истинно, то β также истинно. Мы говорим, что α эквивалентно β, если α истинно в точности в тех же случаях, что и β. В действительности, эти понятия могут быть определены через понятия 'и', 'или', 'не'. А именно:

α-›β значит то же самое, что (~α)#β

α‹-›β значит то же самое, что и (α&β)#(~α&~β)

α‹-›β также значит то же самое, что и (α-›β)&(α-›β)

До сих пор ничего не было сказано о том, что значат переменные, входящие в состав высказывания. В действительности, использование переменных имеет смысл лишь в случае, когда они вводятся с помощью кванторов. Кванторы позволяют делать высказывания о множествах объектов и формулировать утверждения, истинные для этих множеств. В исчислении предикатов имеются два квантора. Если ν обозначает переменную, а ρ – это произвольное высказывание, то коротко значение кванторов можно выразить так:

Первый из кванторов называется квантором общности, так как он указывает на все объекты, существующие во вселенной («для всех ν,…»). Второй квантор называется квантором существования, так как он указывает на существование некоторого объекта (или объектов) («существует ν такой что…»). В качестве примера приведем формулу

all(X, мужчина(Х) -› человек(Х))

которая значит, что какое бы значение X мы не выбрали, если X является мужчиной, то тогда X – человек. Эту формулу можно прочитать так: для любого X, если X является мужчиной, то X является человеком. Или в более простой формулировке: каждый мужчина является человеком. Аналогично

exists(Z, отец(джон,2)& женщина(Z)))

значит, что существует объект, обозначаемый Z такой, что Джон является отцом Z и Z – женщина. Эту формулу можно прочитать так: существует Z такой, что Джон является отцом Z и Z – женщина. Или в более естественной формулировке: Джон имеет дочь. Ниже приведены две более сложные формулы исчисления предикатов:

all(X, животное(Х) -› exists(Y,мать(X,Y)))

all(X, формула_исчисления_предикатов(Х) ‹-› атомарная_формула(Х) # составная_формула(Х))

Как было показано в предыдущем разделе, формулы исчисления предикатов, записанные с использованием связок -› (импликация) и ‹-› (эквивалентность), могут быть переписаны лишь с использованием связок& (конъюнкция), # (дизъюнкция) и ~ (отрицание). В действительности, существует множество разных форм записи формул, и мы ни в коей мере не принесли бы в жертву выразительность формул, если бы должны были полностью отказаться от использования, например, #, -›, ‹-› и exists(X, P). Как следствие этой избыточности, существуют много различных способов записи одного и того же высказывания. При необходимости выполнять формальные преобразования формул исчисления предикатов это оказывается очень неудобным. Было бы значительно лучше, если бы все, что мы хотим сказать, можно было выразить единственным способом. Поэтому здесь будет рассмотрен способ преобразования формул исчисления предикатов к специальному виду – стандартной форме, - обладающему тем свойством, что число различных способов записи одного и того же утверждения меньше по сравнению с использованием других форм. В действительности будет показано, что высказывание исчисления предикатов, представленное в стандартной форме, очень похоже на некоторое множество утверждений языка Пролог. Так что исследование стандартной формы имеет существенное значение для понимания связи между Прологом и математической логикой. В приложении В будет коротко описана программа на Прологе, автоматически транслирующая формулы исчисления предикатов в стандартную форму.

Процесс приведения формулы исчисления предикатов к стандартной форме состоит из шести основных этапов.

Процедура начинается с замены всех вхождений -› и ‹-› в соответствии с их определениями, данными в разд. 10.1. Так, например, формула

аll(Х,мужчина(Х) -› человек(Х))

будет преобразована в формулу

аll(Х,~мужчина(Х) # человек(Х))

На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. Если такой случай имеет место, то формула переписывается по соответствующим правилам. Так, например, формула

~(человек (цезарь)& существующий (цезарь))

преобразуется в

~человек(цезарь) # существующий (цезарь)

а

~аll(Х, человек (X))

преобразуется в

exists(Х,~человек(Х))

Преобразования, выполняемые на втором этапе, основаны на следующих фактах:

~(α&β) значит то же самое, что и (~α) # (~β)

~exists(ν,ρ) значит то же самое, что и all(ν,~ρ)

~all(ν,ρ) значит то же самое, что и exists(ν,~ρ)

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

На следующем этапе удаляются кванторы существования. Это делается путем введения новых констант – сколемовских констант - вместо переменных связанных (введенных) квантором существования. Вместо того чтобы говорить, что существует объект, обладающий некоторым множеством свойств, можно ввести имя для такого объекта и просто сказать, что он обладает данными свойствами. Это соображение лежит в основе введения сколемовских констант. Сколемизация более существенно изменяет логические свойства формулы, чем все обсуждавшиеся ранее преобразования. Тем не менее, она обладает следующим важным свойством. Если имеется формула, то интерпретация, в которой эта формула истинна, существует тогда и только тогда, когда существует интерпретация, в которой истинна формула, полученная из первой в результате сколемизации. Такая форма эквивалентности формул вполне достаточна для наших целей. Так, например, формула

exists(X,женщина(X)& мать(Х,ева))

в результате сколемизации преобразуется в формулу

женщина(g1)& мать(g1, ева)

где g1 – некоторая новая константа, не использовавшаяся ранее. Константа g1 представляет некоторую женщину, мать которой есть Ева. То, что для обозначения константы использован символ» отличный от использовавшихся ранее, существенно, так как в высказывании ничего не говорится о том, что какой-то конкретный человек является дочерью Евы. В утверждении говорится лишь о том, что такой человек существует. Может оказаться, что g1 будет соответствовать тот же самый человек, который соответствует другой константе, но это уже дополнительная информация, никак не выраженная в высказывании.

Если формула содержит кванторы общности, то процедура сколемизации уже не столь проста. Например, если в формуле ^[17]

аll(Х, человек(Х) -› exists(Y,мать(X,Y)))

(«каждый человек имеет мать») заменить каждое вхождение переменной V, связанной квантором существования, на константу g2 и удалить квантор существования, то получится:

all(X, человек(Х) -› мать(X,g2))

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

all(X, человек(Х) -› мать(Х, g2(Х)))

В этом случае функциональный символ g2 соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.

Этот этап очень прост. Каждый квантор общности просто выносится в начало формулы. Это не влияет на значение формулы. Так, например, формула

all(X, мужчина(Х) -› аll(Y,женщина(Y) -› нравится (X,Y)))

преобразуется в

аll(Х, аll(Y,мужчина(Х) -› (женщина(Y) -› нравится (X,Y))))

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

аll(Х,живой(Х) # мертвый(Х)& аll(Y,нравится(мэри,Y) #грязный(Y))

теперь можно представить так:

(живой(Х) # мертвый(Х))& (нравится(мэри,Y) # грязный (Y))

Эта формула значит, что, какие бы X и Y ни были выбраны, либо X живой, либо X мертвый, и либо Мэри нравится Y, либо Y – грязный.

На этом этапе исходная формула исчисления предикатов претерпела довольно много изменений. Формула больше не содержит в явном виде кванторов, а из логических связок в ней остались лишь & и # (помимо отрицания, входящего в состав литералов). Теперь формула преобразуется к специальному виду - конъюнктивной нормальной форме, характерной тем, что дизъюнктивные члены формулы не содержат внутри себя конъюнкцию. Таким образом, формулу можно преобразовать к такому виду, когда она будет представлять последовательность элементов, соединенных друг с другом конъюнкциями, а каждый элемент является либо литералом, либо состоит из нескольких литералов, соединенных дизъюнкцией. Чтобы привести формулу к такому виду, необходимо использовать следующие два тождества:

(А&В) # С эквивалентно (А # С)&(В # С)

А # (В&С) эквивалентно (А # В)&(А # С)

Так, например, формула:

выходной(Х) # (работает(крис, X) & (сердитый (крис) # унылый(крис)))

(Для каждого X либо X – выходной день, либо Крис работает в день X и при этом он либо сердитый, либо унылый) эквивалентна следующей:

выходной(Х) # (работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))

(Для каждого X, во-первых, X является выходным днем или Крис работает в день X; во-вторых, либо X – выходной день, либо Крис сердитый или унылый).

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

(А & В) & (С & (D & Е))

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

(А & В) & (С & (D & Е)) А & (( В& С) & (D & Е)) (А & В) & ((С & D) & Е)

обозначают одно и то же. И хотя структурно эти формулы различны, они имеют один и тот же смысл. Это объясняется тем, что если установлена истинность всех высказываний из некоторого множества, то не имеет значения каким образом они группируются в сложное конъюнктивное высказывание. Не имеет значения, например, как сказать «А истинно и В и С также истинны» или «А и В истинны и С тоже истинно». Следовательно, скобки никак не влияют на смысл формулы. Можно просто написать (неформально):

A & B & C & D & E

Далее, порядок записи этих формул также не имеет значения. Безразлично, как сказать: «А и В истинны» или «В и А истинны», так как оба эти высказывания имеют одно и то же значение. И наконец, нет необходимости указывать знак конъюнкции (&) между формулами, так как заранее известно, что на верхнем уровне формула является конъюнкцией составляющих ее частей. Поэтому, в действительности, значение представленной формулы можно выразить значительно короче, представив ее в виде совокупности {А, В, С, D, Е}. Название «совокупность» подчеркивает, что порядок элементов не имеет значения. Совокупность {А, В, С, D, Е} в точности то же самое, что и {В, А, С, Е, D}, {Е, D, В, С, А} и так далее. Формулы, являющиеся элементами совокупности, полученной в результате преобразования некоторой формулы исчисления предикатов, называются дизъюнктами. Таким образом, каждая формула исчисления предикатов эквивалентна (в некотором смысле) совокупности дизъюнктов.

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

((V # W) # X) # (Y # Z)

где переменные являются литералами. Теперь те же самые рассуждения, которые были сделаны о структуре формулы на верхнем уровне, можно применить к дизъюнктам. Как и выше, скобки не влияют на значение дизъюнкта. Точно так же несуществен и порядок литералов. Таким образом, можно просто сказать, что дизъюнкт – это совокупность литералов (неявно соединенных дизъюнкцией). В последнем примере это будет {V, W, X, Y, Z}

Теперь исходная формула представлена в стандартной форме. Более того, использовавшиеся для преобразования правила не зависят от того, существует или нет интерпретация, при которой формула истинна. Стандартная форма состоит из совокупности дизъюнктов, каждый из которых представляет совокупность литералов. Литерал – это либо атомарная формула, либо отрицание атомарной формулы. Эта форма является достаточно лаконичной, так как в ней опущены логические связки конъюнкций, дизъюнкций и кванторы всеобщности. Но при этом, очевидно, следует помнить о принятых соглашениях. И каждый раз, имея дело со стандартной формой, понимать, где и что в ней опущено. Рассмотрим, что представляет собой стандартная форма некоторых формул (предполагается, что уже выполнены первые пять этапов преобразования). Прежде всего вернемся к уже рассматривавшемуся примеру:

(выходной(Х) # работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))

Эта формула порождает два дизъюнкта. Первый дизъюнкт содержит литералы:

выходной(Х), работает(крис,Х)

а второй литералы:

выходной(Х), сердитый(крис), унылый(крис)

Другой пример. Формула

(человек(адам)& человек(ева))&

((человек(Х) # ~мать(Х,Y)) # ~человек(#))

дает три дизъюнкта. Два из них содержат по одному литералу каждый

человек (адам)

и

человек (ева)

Другой содержит три литерала:

человек(Х), ~мать(Х,Y), ~человек(Y)

В заключении этого раздела рассмотрим еще один пример, демонстрирующий все этапы приведения формулы к стандартному виду. Начнем с формулы

all(X, аll(Y,человек(Y) -› почитает(Y,Х) -› король(Х))

утверждающей, что, если все люди относятся с почтением к некоторому человеку, то этот человек является королем. (Для каждого X, если каждый Y является человеком, почитающим X, то X – это король). После устранения импликации (этап 1) получаем:

аll(Х,~(аll(Y,~человек(Y) # почитает(Y,Х))) # король(Х))

Перенос отрицания внутрь формулы (этап 2) приводит к следующему:

аll(Х,ехists(Y,человек(Y) & ~почитает(Y,Х)) # король(Х))

Затем, в результате сколемизации (этап 3) формула преобразуется к виду:

аll(Х,(человек(f1(Х)) & ~почитает(f1Х),Х)) # король(Х))

где f1 -сколемовская функция. Теперь производится удаление кванторов всеобщности (этап 4), что приводит к формуле;

(человек(f1(X)) & ~почитает(f1(Х),X)) # король(Х)

Затем формула преобразуется к конъюнктивной нормальной форме (этап 5), в которой конъюнкция не появляется внутри дизъюнктов:

(человек(f1(Х) # король(Х)) & (~почитает(f1(Х), X) # король(Х))

Эта формула содержит два дизъюнкта (этап 6). Первый дизъюнкт имеет два литерала:

человек(f1(Х)), король(Х)

а второй дизъюнкт имеет литералы:

почитает(f1(Х),Х), король(Х)

Очевидно, что для записи формул, представленных в стандартной форме, необходим соответствующий способ. Рассмотрим его. Прежде всего, стандартная форма представляет совокупность дизъюнктов. Договоримся записывать дизъюнкты последовательно один за другим, помня при этом, что порядок записи не имеет значения. В свою очередь, дизъюнкт является совокупностью литералов, часть из которых содержит отрицание, а часть не содержат его. Примем соглашение записывать сначала литералы без отрицания, а затем литералы с отрицанием. Эти две группы литералов будем разделять знаком ':-'. Литералы без отрицания при записи будем отделять друг от друга точкой с запятой (;) (помня, конечно, при этом, что порядок записи литералов в каждой группе неважен), а литералы с отрицанием будем записывать без знака отрицания (~), разделяя литералы запятыми. Запись каждого дизъюнкта будет заканчиваться точкой. При такой форме записи дизъюнкт, содержащий отрицания литералов K, L,… и литералы А, В,… мог бы быть представлен так:

A; B;…:- K, L,…

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

(А # В #…) # (~К # -L #…)

что эквивалентно

(A # B # …) # ~(K & L & …)

Это в свою очередь эквивалентно (К & L &…) -› (А # В #…)

Если записать ',' вместо 'и', ';' вместо 'или' и ':-' вместо 'является следствием', то дизъюнкт естественным образом примет следующий вид:

A; B;…:- K, L,…

С учетом этих соглашений формула

(человек(адам) & человек(ева)) &((человек(Х) # ~мать(Х,Y)) # ~человек(Y))

записывается так:

человек(адам):-.

человек(ева):-.

человек(Х):- мать(Х,Y), человек(Y).

Это выглядит уже довольно знакомо. В действительности, это выглядит в точности как определение на Прологе того, что значит быть человеком. Однако другие формулы дают более загадочный результат. Так, для примера о выходном дне имеем:

выходной(Х); работает(крис,X):-.

выходной(Х); сердитый(крис); унылый(крис):-.

Сразу не так очевидно, чему это может соответствовать в Прологе. Этот вопрос будет подробнее рассмотрен в следующем разделе.

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

человек(f1(X)); король(Х):-.

король(Х):- почитает(f1(Х),Х).

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

В 60-х годах в этой области наблюдалась большая активность, связанная с возможностью использования вычислительных машин для автоматического доказательства теорем. Именно эта область научной деятельности, по-прежнему остающаяся источником новых идей и методов, дала жизнь идеям, легшим в основу Пролога. Одним из фундаментальных достижений того времени явилось открытие Дж. А. Робинсоном принципа резолюций и его применение к автоматическому доказательству теорем. Резолюция – это правило вывода, говорящее о том, как одно высказывание может быть получено из других. Используя принцип резолюций, можно полностью автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь решать, к каким из высказываний следует применять правило вывода, а правильные следствия из них будут строиться автоматически.

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

Из

унылый(крист); сердитый(крис):- рабочий_день(сегодня), идет_дождь(сегодня).

и

неприятный(крис):- сердитый(крис), усталый(крис).

следует

унылый(крис); неприятный(крис):- рабочий_день(сегодня), идет_дождь(сегодня), усталый(крис).

На естественном языке это звучит так. Если сегодня рабочий день и идет дождь, то Крис – унылый или сердитый. Кроме того, если Крис сердитый и усталый, то он неприятен. Поэтому, если сегодня рабочий день, идет дождь и Крис усталый, то Крис является унылым или неприятным.

В действительности, мы сильно упростили ситуацию, опустив два момента. Прежде всего, ситуация усложняется, когда дизъюнкты содержат переменные. В такой ситуации две атомарные формулы не обязательно должны быть идентичными – они должны быть лишь «сопоставимы». Кроме того, дизъюнкт, являющийся следствием двух других дизъюнктов, получается в результате их соединения (с удалением повторяющейся формулы) с помощью некоторой дополнительной операции. Эта операция включает в себя «конкретизацию» переменных до такой степени, чтобы две сопоставляемые формулы стали идентичными. Используя терминологию Пролога, можно сказать, что, если имелось два дизъюнкта, представленных в виде структур, и было выполнено сопоставление соответствующих подструктур, то результат соединения этих структур и был бы представлением нового дизъюнкта. Второе упрощение состоит в том, что в общем случае, правило резолюций допускает сопоставление нескольких литералов в правой части одного дизъюнкта с несколькими литералами в левой части другого дизъюнкта. Здесь будут рассматриваться лишь примеры, когда из каждого дизъюнкта выбирается один литерал.

Рассмотрим один пример применения правила резолюций при наличии переменных:

человек(f1(Х)); король(Х):-. (1)

король(Y):- почитает(f1(Y),Y). (2)

почитает(Z,артур):- человек(Y). (3)

Два первых дизъюнкта представляют стандартную форму формулы, которую можно выразить так: «если каждый человек почитает кого-то, то этот кто-то – король». Переменные переименованы для удобства объяснения. Третий дизъюнкт выражает высказывание о том, что каждый человек почитает Артура. Применяя правило резолюций к (2) и (3) (сопоставляя два соответствующих литерала), получаем:

король(артур):- человек(f1(артур)). (4)

(Y в (2) сопоставлен с артур в (3), a Z в (3) сопоставлен с fl(Y) в (2)). Теперь можно применить правило резолюций к (1) и (4), что дает:

король(артур); король(артур):-.

Это эквивалентно факту, гласящему, что Артур является королем.

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

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

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

:-.

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

Каким образом это свойство метода резолюций может помочь нам? Имеет место следующий факт:

Если множество формул {А₁, A₂,…, А_n} совместно, то формула В является следствием формул {A_l, A₂,…, A_n} тогда и только тогда, когда множество формул {А₁, A₂,…, А_n ⌉В} - несовместно.

Таким образом, если множество гипотез совместно, то необходимо лишь добавить к нему дизъюнкты, соответствующие отрицанию высказывания, которое следует доказать. Резолюция даст пустой дизъюнкт в точности тогда, когда доказываемое высказывание следует из данных гипотез. Дизъюнкты, добавляемые к множеству гипотез, называются целевыми дизъюнктами. Отметим, что целевые дизъюнкты ничем не отличаются от гипотез – и те и другие являются дизъюнктами. Так что, если задано множество дизъюнктов {А₁, А₂, …, А_п} и требуется проверить несовместность этого множества дизъюнктов, то в действительности невозможно определить, идет ли речь о доказательстве того, что ⌉А₁ следует из A₂, А₃, …, А_п или что ⌉А₂ следует из A₁, A₃, …, А_n, или что ⌉А₃ следует из А₁, А₂, A₄,…, А_n и так далее. Именно это является причиной того, что необходимо указывать какие дизъюнкты в действительности являются целевыми дизъюнктами. Для системы, использующей метод резолюций, все перечисленные задачи эквивалентны.

Легко увидеть, как можно получить пустой дизъюнкт в примере с королем Артуром, если добавить целевой дизъюнкт:

:- король(артур). (5)

(это дизъюнкт для ~король(артур)). Ранее уже было показано, как дизъюнкт

король(артур); король(артур):-. (6)

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

король(артур):-. (7)

И наконец, резолюция дизъюнктов (6) и (7) дает

:-.

Таким образом, использование метода резолюций позволило доказать следствие, что Артур является королем.

Полнота метода резолюций является полезным математическим свойством. Это свойство означает, что, если некоторый факт следует из гипотез, то имеется возможность доказать его истинность (показав несовместность множества дизъюнктов, содержащего гипотезы и отрицание доказываемого факта)» используя для этого метод резолюций. Однако, когда мы говорим, что методом резолюций можно вывести пустой дизъюнкт, это значит, что существует последовательность шагов, на каждом из которых правило резолюций применяется к аксиомам или к дизъюнктам выведенным на предыдущих шагах, и эта последовательность заканчивается выводом дизъюнкта, не содержащего литералов. Единственная проблема – найти соответствующую последовательность шагов. Так как, хотя метод резолюций и говорит о том, как получить следствие двух дизъюнктов, он не сообщает, какие дизъюнкты выбрать для очередного шага и какие литералы в этих дизъюнкциях необходимо «сопоставить». Обычно, если имеется большое количество гипотез, то существует и много вариантов выбора среди них. Более того, на каждом шаге выводится новый дизъюнкт и он тоже становится кандидатом на участие в последующей обработке. Большинство из имеющихся возможностей выбора дизъюнктов и литералов в них не имеют отношения к решаемой задаче и, если не производить тщательного отбора среди кандидатов, то можно потратить слишком много времени на бесплодные поиски, а путь, ведущий к решению, так и не найти.

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

10.5. Хорновские дизъюнкты

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

Прежде всего, очевидно, что существуют два вида хорнов-ских дизъюнктов – дизъюнкты, содержащие один литерал без отрицания и дизъюнкты, не содержащие таких литералов. Будем называть эти два типа хорновских дизъюнктов соответственно дизъюнктами с заголовком и дизъюнктами без заголовка. Следующие примеры иллюстрируют указанные типы дизъюнктов (необходимо помнить, что литералы без отрицания записываются слева от знака ':-'):

холостяк(Х):- мужчина(Х), неженат(Х).

:- холостяк(Х).

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

• Имеется только один дизъюнкт без заголовка. Все остальные дизъюнкты имеют заголовки.

Так как совершенно не имеет значения, какие дизъюнкты считать целевыми, то можно принять решение рассматривать дизъюнкт без заголовка как целевой, а все остальные дизъюнкты – как гипотезы. Такое решение выглядит довольно естественно.

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

Давайте подведем итог и посмотрим, как Пролог вписывается в рассмотренную выше схему. Как было показано, некоторые формулы, представленные в виде совокупности дизъюнктов, выглядят в точности так же, как и утверждения в Прологе, в то время как другие формулы имеют несколько отличный вид. Формулы, имевшие вид утверждений Пролога, есть в действительности не что иное, как формулы, представимые в виде хорновских дизъюнктов. При записи хорновского дизъюнкта в соответствии с принятыми соглашениями, количество атомарных формул слева от знака ';-' не может превышать одну. В общем случае, дизъюнкты могут иметь несколько таких формул (они соответствуют литералам, представляющим атомарные формулы без отрицания). В Прологе непосредственно можно представить только хорновские дизъюнкты. Утверждения программы на Прологе соответствуют хорновским дизъюнктам с заголовком (в рамках определенной процедуры доказательства теорем). А что в Прологе соответствует целевому дизъюнкту? Очень просто, вопрос в Прологе

?- A₁, A₂,…, A_n

в точности соответствует хорновскому дизъюнкту без заголовка:- A₁, A₂,…, А_п

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

Пролог-система основывается на процедуре доказательства теорем методом резолюций для хорновских дизъюнктов. Конкретная стратегия, используемая при этом, является разновидностью линейной входной резолюции. При использовании этой стратегии, выбор дизъюнктов для резолюции на каждом шаге ограничен следующими условиями. Процедура начинается с применения правила резолюций к целевому дизъюнкту и к одной из гипотез, что дает новый дизъюнкт. Затем производится резолюция этого дизъюнкта и одной из гипотез, что дает еще один новый дизъюнкт. Затем правило резолюций применяется к последнему полученному дизъюнкту и к одной из гипотез и так далее. На каждом этапе правило резолюций применяется к последнему из вновь полученных дизъюнктов и к одной из исходных гипотез. Правило резолюций никогда не применяется, если оба дизъюнкта были выведены на предыдущих этапах или являются исходными гипотезами. С точки зрения Пролога, последний выведенный дизъюнкт можно рассматривать как конъюнкцию целевых утверждений, которые еще надо доказать (согласовать с базой данных). В начальный момент это вопрос, а в конце процесса, при благоприятных условиях,- это пустое утверждение. На каждом этапе ищется утверждение, заголовок которого сопоставим с одним из целевых утверждений. Если необходимо, происходит конкретизация переменных. Удаляется целевое утверждение, с которым произошло сопоставление, а затем к целевым утверждениям, которые необходимо согласовать, добавляется тело найденного утверждения, в котором произведена конкретизация переменных. Так, например, начав с вопроса

:- мать(джон,Х), мать(Х,Y).

и утверждения

мать(U,V):- родитель(U,V), женщина(V).

получаем

:- родитель(джон,Х), женщина(Х), мать(Х,Y).

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

Все сказанное относится к событиям, происходящим после того, как Пролог выбрал утверждение для сопоставления с первой целью. Но как организуется исследование альтернативных утверждений для удовлетворения той же самой цели? В Прологе используется стратегия поиска вглубь, а не поиска вширь. Это значит, что Пролог в каждый момент времени рассматривает лишь одну альтернативу, упорно следуя подразумеваемому предположению о правильности сделанного выбора. Выбор утверждений для каждой цели производится в строго фиксированном порядке, а пересмотр выбранных ранее утверждений происходит лишь в случае, когда все последующие попытки не привели к решению. В качестве альтернативы можно было бы предложить стратегию, при которой система запоминает одновременно все альтернативные пути решения. При этом система переходила бы по кругу от одной альтернативы к другой, прослеживая каждую альтернативу на небольшую глубину, а затем переходя к следующей. Такая стратегия поиска вширь имеет одно преимущество – если решение существует, то оно обязательно будет найдено. Используемая в Прологе стратегия поиска вглубь может привести к «зацикливанию» и, следовательно, никогда не будут исследованы некоторые альтернативы. С другой стороны такая стратегия намного проще и требует меньших затрат памяти при реализации на вычислительных машинах с традиционной архитектурой.

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

равны(X,X).

?- равны(foo(Y),Y).

Это возможно по той причине, что в Прологе разрешается сопоставлять некоторый терм с его собственным подтермом. В этом примере foo(Y) сопоставляется с Y, который сам является частью этого терма. В результате этого Y становится равным foo(Y) что в свою очередь равно foo(foo(Y)) (учитывая значение Y), что равно foo(foo(foo(Y))) и так далее. Так что в результате Y обозначает некоторую бесконечную структуру. Заметим, что хотя Пролог-системы могут допускать использование подобных конструкций, большинство из них будут не в состоянии напечатать окончательный результат сопоставления. В соответствии с формальным определением унификации, подобного вида «бесконечные термы» никогда не должны появляться. Так что, Пролог выполняет эту процедуру неправильно в сравнении с тем, как это делается при доказательстве теорем методом резолюций. Для того чтобы сделать процедуру корректной, необходимо добавить проверку условия, заключающегося в том, что переменная не может быть конкретизирована некоторым значением, содержащим эту переменную. Такая проверка, проверка на вхождение, не представляла бы труда для ее реализации, но значительно замедляла бы выполнение программы на Прологе. Так как число программ, в которых может встретиться такая конструкция, невелико, то в большинстве реализаций такая проверка просто не делается.

В нескольких последних разделах было показано, как используются в Прологе идеи доказательства теорем. Можно видеть, что наши программы довольно похожи на гипотезы о проблемной области, а вопросы очень похожи на теоремы, которые нам хотелось бы доказать. Таким образом, программирование на Прологе имеет мало общего с процессом выдачи машине указаний о том, что и когда следует делать. Оно скорее состоит в передаче машине информации, которая предполагается истинной, и обращении к ней с вопросами о возможных следствиях из этой информации. Идея о том, что программирование должно выглядеть именно так, привлекательна и она привела многих специалистов к исследованию концепции логического программирования, то есть программирования на языке логики, как практической альтернативы обычному. Такой подход резко отличается от использования традиционных языков программирования подобных Фортрану или Лиспу, при программировании на которых необходимо как можно более подробно описать что и когда должна делать вычислительная машина. Преимущества логического программирования должны проявиться в том, что программы станут более понятными. Они не будут содержать затрудняющие понимание детали относительно того как решать задачу, а скорее будут напоминать описание того, что собой представляет результат решения. Кроме этого, если программа выглядит как описание (спецификация) того, что предполагается получить, то и относительно проще проверить (вручную или, возможно, используя какие-то автоматические средства), делает ли она в действительности то, что требуется. Подводя итог, можно сказать: преимущества языка логического программирования были бы следствием того, что программы обладают как декларативной семантикой, так и процедурной. Мы бы знали что программа вычисляет, а не как она это делает. Мы не будем здесь рассматривать логическое программирование вообще. Интересующемуся этим вопросом читателю рекомендуем обратиться к книге Ко-walski R. Logic for Problem Solving, North Holland, 1979.

Давайте рассмотрим Пролог как кандидата на место языка логического программирования и посмотрим, насколько хорошо он для этого подходит. Прежде всего, ясно, что некоторые программы на Прологе действительно представляют описание проблемной области на языке логики. Запись:

мать(Х,Y):- родитель(Х,Y), женщина(Y).

можно рассматривать как описание того, что значит быть матерью (это значит быть женщиной и быть одним из родителей). Это утверждение выражает высказывание, которое, как мы предполагаем, должно быть истинным, и, кроме того, указывает, как показать, что кто-то является матерью. Аналогично, утверждения;

присоединить([], X, X).

присоединить([А|В],С[А|D]):- присоединить (B,C,D).

говорят о том, что собой представляет добавление одного списка в начало другого списка. Если пустой список помещается в начало некоторого списка X, то результатом будет X. С другой стороны, если непустой список присоединяется в начало некоторого списка, то головой списка-результата будет голова присоединяемого списка. Кроме того, хвостом списка-результата будет список, получаемый в результате присоединения хвоста первого списка ко второму списку. Можно считать, что эти утверждения описывают отношение присоединить, так же как и (возможно) то, как в действительности присоединить один список к другому.

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

memberl(X, List):- var(List),!,fail.

memberl(X,[X|_]).

memberl(X,[_|List]):- memberl(X,List).

print(0):-!.

print(N):- write(N), N1 is N-1, print(N1).

noun(N):- name(N,Name1), append(Name2, [ll5],Namel), name(RootN,Name2), noun(RootN).

implies(Assum,Concl):-asserta(Assum), call(Concl), retract(Concl).

Эта проблема имеет место для всех «встроенных» предикатов, используемых в программах на Прологе. Предикат подобный Var(List) ничего не говорит о принадлежности элемента списку, а проверяет состояние переменной (является ли указанная переменная неконкретизированной), возникающее в процессе доказательства. Аналогично, «отсечение» говорит кое-что о доказательстве высказывания (выбор каких альтернатив можно игнорировать), а не о самом этом высказывании. Два указанных «предиката» можно рассматривать как способ выражения управляющей информации о том, как должно выполняться доказательство. Точно так же, предикаты подобные write(N) не имеют каких-либо интересных логических свойств, но заранее предполагают, что в ходе доказательства будет достигнуто определенное состояние (N конкретизируется) и начинают обмен информацией с программистом, сидящим за терминалом. Целевое утверждение name(N, Name1) говорит кое-что о внутренней структуре объекта, который в исчислении предикатов был бы неделимым символом. В Прологе можно преобразовывать символы в строки литер, структуры в списки и в утверждения. Эти операции нарушают замкнутость высказываний исчисления предикатов. В последнем примере, использование предиката asserta означает, что правило, о котором идет речь, добавляет что-то к множеству аксиом. В логике каждое правило или факт сохраняет истинность независимо от того, существуют ли какие либо другие факты или правила. В данном случае мы имеем дело с правилом, которое грубо нарушает этот принцип. Кроме того, если мы используем это правило, то окажемся в ситуации, когда на разных этапах доказательства имеется различное множество аксиом. Наконец, то что в одном из правил предполагается использовать терм Concl в качестве целевого утверждения, означает, что допускается, чтобы переменная обозначала высказывание, встречающееся в некоторой аксиоме. Такая конструкция не относится к числу тех, которые могут быть выражены на языке исчисления предикатов, но напоминает возможности, которые могут быть представлены логикой более высокого порядка.

На приведенном примере можно видеть, что некоторые программы на Прологе, можно понять лишь в терминах, описывающих что и когда может произойти при выполнении программ и каким образом программы сообщают системе о том, что нужно делать. В качестве крайнего случая, можно привести программу для генатом представленную в гл. 7. Вряд ли вообще может быть дана какая-либо декларативная интерпретация этой программы. Имеет ли тогда смысл рассматривать Пролог как язык логического программирования? Можем ли мы реально надеяться на какие-то преимущества логического программирования применительно к нашим программам на Прологе? На оба этих вопроса можно дать положительный ответ и основанием для этого служит то, что приняв соответствующий стиль программирования, мы все же можем получить некоторые преимущества благодаря связи Пролога с логикой. Ключевым моментом является использование разбиения программ на части, ограничивающие использование нелогических операций небольшим множеством утверждений. В качестве примера в гл. 4 было показано, как в некоторых случаях «отсечение» может быть заменено предикатом not. В результате таких замен, программу, содержавшую целый ряд «отсечений» можно свести к программе, в которой «отсечение» используется лишь однажды (в определении not). Использование предиката not даже если он не совсем точно соответствует логическому '~' позволяет восстановить часть логической основы программы. Аналогично, ограничивая область применения предикатов asserta и retract определениями небольшого числа предикатов (таких как генатом и найтивсе), можно добиться того, что в целом программа становится более понятной по сравнению с программой, в которой эти предикаты свободно используются где угодно.

Таким образом, с появлением Пролога конечная цель, состоящая в создании языка логического программирования, не была достигнута. Тем не менее, Пролог дал практическую систему программирования, обладающую в некоторой степени свойствами, которыми должен обладать язык логического программирования – ясностью и декларативностью. Между тем ведутся работы по разработке улучшенных версий Пролога, которые более близки к логике чем имеющиеся в настоящее время. К числу наиболее важных работ в этой области относятся работы по созданию практической системы программирования, в которой нет необходимости использовать «отсечение» и которая имеет вариант предиката not точно соответствующий логическому понятию отрицания.

Примечания:

1

В книге термин «Пролог» употребляется в трех значениях: 1) Пролог – язык программирования с совокупностью синтаксических и семантических правил записи программ; 2) Пролог – программная система (интерпретатор), реализующая язык; эта система и осуществляет диалог с пользователем; 3) Пролог – машина, на которой Пролог-система выполняет (интерпретирует) программы, написанные на языке Пролог. Как правило, из контекста всегда ясно, какое значение используется в каждом конкретном случае. При необходимости явного указания при переводе использовались термины: «язык Пролог», «Пролог-система», «Пролог-машина». - Прим. пepeв.

15

Имеется перевод: Мендельсон Э. Введение в математическую логику.- М.: Наука, 1971.- Прим. перев.

16

Имеется перевод: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.- М.: Наука, 1983.- Прим. перев.

17

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