Принцип резолюции в исчислении высказываний и логике предикатов и его модификации

     Стерлинг  и Шапиро в книге "Искусство  программирования на языке Пролог" пишут: "Зрелость языка означает, что он больше не является доопределяемой и уточняемой научной концепцией, а становится реальным объектом со всеми присущими ему пороками и добродетелями. Настало время признать, что хотя Пролог и не достиг высоких целей логического программирования, но, тем не менее, является мощным, продуктивным и практически пригодным формализмом программирования". 

 

      3. Исчисление высказываний. 

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

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

     (S. U) ЕслиU является атомом, то у является  ППФ.

     (S¬)  Если U является ППФ, то —U также является ППФ.

     (S. v) Если U и ф являются ППФ, то (U u ф) также является ППФ.

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

     Выражение -U читается как "не U", а (U v ф) читается как дизъюнкция "U или ф (или оба)". Можно ввести другие логические константы — "л" (конъюнкция), "D" (импликация, или обусловленность), "=" (эквивалентность, или равнозначность), которые, по существу, являются сокращениями комбинации трех приведенных выше констант. .

     (U ^ ф) Эквивалентно¬(¬U v ф). Читается "U и ф".

     (U ф) Эквивалентно (¬U v ф). Читается "U имплицирует ф".

     (U==ф)  Эквивалентно (U ф)^(ф U). Читается "U эквивалентно ф".

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

     ¬(U^ф) преобразуется в (¬Uv¬ф), ¬(U v ф) преобразуется  в (-U^ф) , ¬¬U преобразуется в U .

     Последний этап преобразований — внесение дизъюнкций внутрь скобок: (Ј v (U ^ф))) заменяется ((ЈvU\(U)^(Јvф)).

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

     ¬(pvq) (-p^A-q) Исходное выражение.

     ¬¬(pvg)v(-p^- q) Исключение~.

     (pvq)v(-p^- q) Ввод - внутрь скобок.

     (¬pv(pvq))v(¬pv(pvq)) Занесение v внутрь скобок.

     {{-p, р, q}, {¬q, р, q} } Отбрасывание А и  v в конъюнктивной нормальной  форме.

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

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

     преобразуется в две фразы:

     p,q<¬q.

     в которых позитивные литералы сгруппированы  слева от знака стрелки, а негативные справа.

     Более строго, фраза представляет собой выражение вида

     в котором p1..., рт q1,..., qn являются атомарными формулами, причем т=>0 и п=>0. Атомы  в множестве р1,..., рт представляют заключения, объединенные операторами  дизъюнкции, а атомы в множестве q1 ..., qn — условия, объединенные операторами  конъюнкции. 

     3.1 Исчисление предикатов 

     Исчисление  высказываний имеет определенные ограничения. Оно не позволяет оперировать  с обобщенными утверждениями  вроде "Все люди смертны". Конечно, можно обозначить такое утверждение  некоторой пропозициональной константой р, а другой константой q обозначить утверждение "Сократ — человек". Но из (р л q) нельзя вывести утверждение "Сократ смертен".

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

     Аргументы могут быть отдельными константами, или составным выражением "функция-аргумент", которое обозначает сущности некоторого мира интересующих нас объектов, или отдельными квантифицируемыми переменными, которые определены в этом пространстве объектов. Специальные операторы — кванторы — используются для связывания переменных и ограничения области их интерпретации. Стандартными являются кванторы общности (V) и существования (3). Первый интерпретируется как "все", а второй — "кое-кто" (или "кое-что").

     Ниже  приведены синтаксические правила  исчисления предикатов первого порядка.

     Любой символ (константа или переменная) является термом. Если rk является символом k-местной функции и а1 ..., <xk являются термами, то Гk(a1..., ak) является термом.

     (S 40

     Если Tk является символом k-местного предиката

     и а1 ..., ak являются термами,

     то U(а1 ..., ak) является правильно построенной формулой (ППФ).

     (S. -) и (S. v)

     Правила заимствуются из исчисления высказывании.

     (S. V) Если U является ППФ и % является  переменной,

     то (любой Х) U является ППФ.

     Для обозначения используются следующие  символы:

     U — произвольный предикат;

     Г — произвольная функция;

     a — произвольный терм;

     X — произвольная переменная.

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

     Использование квантора существования позволяет  преобразовать термы с квантором  общности в соответствии с определением

     (EX)U определено как -(любой X)-U.

     Выражение (EХ)(ФИЛОСОФ(Х)) читается как "Кое-кто  является философом", а выражение (любой Х)(ФИЛОСОФ(Х)) читается как "Любой  является философом". Выражение ФИЛОСОФ(Х) представляет собой правильно построенную формулу, но это не предложение, поскольку область интерпретации для переменной X не определена каким-либо квантором. Формулы, в которых все упомянутые переменные имеют определенные области интерпретации, называются замкнутыми формулами.

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

     (1) Исключить операторы эквивалентности,  а затем импликации.

     (2) Используя правила Де Моргана  и правила замещения (E X)U на -(любой  X)-U (а следовательно, и (любой X) U на -(E X)-U), выполнить приведение отрицания.

     (3) Выполнить приведение переменных. При этом следует учитывать  особенности определения области  интерпретации переменных кванторами. Например, в выражении (E Х)(ФИЛОСОФ(Х))&(E Х)(АТЛЕТ(Х)) переменные могут иметь разные интерпретации в одной и той же области. Поэтому вынесение квантора за скобки — (E Х)(ФИЛОСОФ(Х))&.(АТЛЕТ(Х))— даст выражение, которое не следует из исходной формулы.

     (4) Исключить кванторы существования.  Кванторы существования, которые появляются вне области интерпретации любого квантора общности, можно заменить произвольным именем (его называют константой Сколема), в то время как экзистенциальные переменные, которые могут существовать внутри области интерпретации одного или более кванторов общности, могут быть заменены функциями Сколема. Функция Сколема— это функция с произвольным именем, которая имеет следующий смысл: "значение данной переменной есть некоторая функция от значений, присвоенных универсальным переменным, в области интерпретации которых она лежит".

     (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 находится в комнате А и, следовательно, переменная имеет экзистенциальную подстановку.

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