Текст книги "Программирование на языке пролог"

Автор книги: У. Клоксин

Соавторы: К. Меллиш
сообщить о нарушении

Текущая страница: 21 (всего у книги 26 страниц)

9.6. Заключение

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

грамматическое правило–› заголовок, ['–›'], тело.

заголовок–› нетерминальный_символ.

заголовок–› нетерминальный_символ, [','], терминальный_символ

тело–› тело, [','], тело.

тело–› тело, [';'], тело.

тело–› элемент_тела.

элемент_тела–› ['!'].

элемент_тела–› ['{'], целевые_утверждения_пролога, ['}'].

элемент_тела–› нетерминальный_символ.

элемент_тела–› терминальный_символ.

Ряд элементов описания неопределен. Здесь приведены их определения на естественном языке.

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

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

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

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

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

Eat your supper.

вставляется дополнительное слово:

You eat your supper.

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

предложение–› императив, группа_существительного, группа_глагола.

императив,[you]–› [].

императив–› [].

Из приведенных здесь правил лишь одно заслуживает внимания. Это первое правило для императив, которое транслируется в утверждение

императив(L,[уоu|L]).

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

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

В заключение рассмотрим пример грамматических правил, используемых для непосредственного извлечения «смысла» предложений, минуя этап построения дерева разбора. Этот пример взят из статьи Pereira, Warren, Artificial Intelligence, v. 13. Представленные далее правила транслируют предложения из ограниченного подмножества предложений английского языка в некоторое представление на языке исчисления предикатов, отражающее смысл этих предложений. Описание исчисления предикатов и используемой формы записи даны в гл. 10. В качестве примера работы программы мы приведем предложение «every man loves a woman» и соответствующую структуру, отражающую его смысл: [14]14
  На «ломаном» русском языке этот пример можно представить следующим образом: «Каждый мужчина нравится некоторая женщина».
  все (X, мужчина (X)–› существует (Y, (женщина (Y) & нравится (X)))) . -Прим. ред.


[Закрыть]

all(X,(man(X)→exists(Y,(woman(Y)& loves(X,Y)))))

Здесь представлены грамматические правила программы:

?– op(100,xfy,&)

?– op(150,xfy,→)

предложение(Р)–› группа_существительного(Х,Р1,Р),группа_глагола(Х,Р1).

группа_существительного(Х,Р1,Р)–›определитель(Х,Р2,Р1,Р),существительное(Х,Р3), отн_утверждение(Х,Р3,Р2).

группа_существительного(Х,Р,Р)–› наст_существительное(Х).

группа_глагола(Х,Р)–› перех_глагол(Х,Y,Р1),группа_существительного(Y,Р1,Р).

группа_глагола(Х,Р)–› неперех_глагол(Х,Р).

отн_утверждение(Х,Р1,(Р1&Р2))–› [that], группа_глагола(Х,Р2).

отн_утверждение(_,Р,Р)–› [].

определитель(Х,Р1,Р2,аll(Х,(Р1>Р2)))–› [every].

определитель(Х,Р1,Р2,ехists(Х,(Р1&Р2)))–› [а].

существительное(Х,man(Х))–› [man].

существительное(Х, woman (X))–› [woman].

наст_существительное(john)–› [john].

пepex_глагол(X,Y,loves(X,Y))–› [loves].

неперех_глагол(Х,lives(Х)))–› [lives].

В этой программе аргументы используются для построения структур, представляющих смысл словосочетаний. Смысл каждого словосочетания определяет последний аргумент соответствующего правила. Однако смысл словосочетания может зависеть от некоторых других факторов, представленных другими аргументами. Например, глагол lives(живет) порождает высказывание вида lives(X),где X– это объект, обозначающий человека, который живет. Смысл слова livesне позволяет заранее определить, чем будет являться X. Чтобы быть полезным, понятие подобное livesдолжно быть применимо к некоторому конкретному классу объектов. Что представляет этот объект, будет определено из контекста, в котором используется глагол lives.Таким образом, имеем следующее определение: для любого X, применение глагола livesк Xимеет смысл lives(X).Слово, подобное every(каждый), является значительно более сложным. В этом случае понятие, соответствующее слову, должно применяться к некоторой переменной и к двум высказываниям, содержащим эту переменную. Результат можно сформулировать так: если подстановка некоторого объекта вместо переменной в первом утверждении делает что-то истинным, то подстановка того же объекта вместо переменной во втором утверждении также сделает что-то истинным.

Упражнение 9.4.Разберитесь в приведенной программе. Попробуйте проследить выполнение программы при обращении к ней с вопросами типа

?– предложение(Х, [every, man, loves, a, woman],[]).

Во что транслируются программой предложения «Every man that lives loves a woman» и «Every man that loves a woman lives». Предложение «Every man loves a woman» является в действительности двусмысленным – может существовать либо единственная женщина, которая нравится каждому мужчине, либо несколько женщин, каждая из которых нравится мужчине. Может ли программа породить альтернативные решения, описывающие смысл каждой из двух указанных интерпретаций предложения? Если нет, то почему? Какое простое предположение о построении структуры, отражающей смысл предложения, было сделано при написании программы?

ГЛАВА 10. ПРОЛОГ И МАТЕМАТИЧЕСКАЯ ЛОГИКА

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

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

10.1. Краткое введение в исчисление предикатов

Если мы намерены обсуждать связь Пролога с математической логикой, то прежде всего необходимо установить, что мы понимаем под логикой. Первоначально логика развивалась как некоторый способ представления определенного класса высказываний, так чтобы можно было, используя формальную процедуру, проверить, справедливы они или нет. Таким образом, логика может быть использована для выражения высказываний, отношений между высказываниями и правил выводаодних высказываний из других. Логическое исчисление специального вида, о котором будет идти речь в этой главе, называется исчисление предикатов.Здесь мы лишь затронем некоторые вопросы исчисления предикатов. Хорошим введением в математическую логику является книга Hodges W. Logic,Penguin Books, 1977. Более подробное обсуждение предмета дано в книге Mendelson E. Intro ductiontoMathematicalLogic,VanNostrandReinhold. [15]15
  Имеется перевод: Мендельсон Э. Введение в математическую логику.– М.: Наука, 1971.– Прим. перев.


[Закрыть]Вы так же можете обратиться к любой книге по математической логике. Другая книга, представляющая интерес, написана Chin L. С, Lee R. С.-Т. Symbolic Logic and Mechanical Theorem Proving,Academic Press, 1973. <sup>[16]16
  Имеется перевод: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.– М.: Наука, 1983.– Прим. перев.


[Закрыть]</sup>

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

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

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

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

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

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

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

Отрицание	⌉α	~α	«не α»
Конъюнкция	α∧β	α&β	«α и β»
Дизъюнкция	α∨β	α#β	«α или β»
Импликация	α⊃β	α-›β	«α влечет β»
Эквивалентность	α≡β	α‹-›β	«α эквивалентна β»

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

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

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

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

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

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

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

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

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

∀ν. ρ	all(ν, ρ)	«ρ истинно для всех значений переменной ν»
∃ν.ρ	exists(ν, ρ)	«существует такое значение переменной ρ, для которого ν истинно»

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

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, формула_исчисления_предикатов(Х) ‹-› атомарная_формула(Х) # составная_формула(Х))

10.2. Приведение формул к стандартной форме

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

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

Этап 1 – исключение импликаций и зквивалентностей

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

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

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

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

Этап 2 – перенос отрицания внутрь формулы

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

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

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

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

а

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

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

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

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

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

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

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

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

Этап 3 – сколемизация

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

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

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

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

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

Если формула содержит кванторы общности, то процедура сколемизации уже не столь проста. Например, если в формуле <sup>[17]17
  В некоторых последующих примерах допущена неточность: в формулах используется импликация, хотя все импликации должны быть удалены на первом этапе.– Прим. перев.


[Закрыть]</sup>

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

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

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

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

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

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

Этап 4 – вынесение кванторов общности в начало формулы

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

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– грязный.

Этап 5 – использование дистрибутивных законов для & и #

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

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

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

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

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

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

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

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

Этап 6 – выделение множества дизъюнктов

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

(А & В) & (С & (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(Х),Х), король(Х)