Исчисление высказываний
8.1.1. Исчисление высказываний
Исчисление высказываний представляет собой логику неанализируемых предположений, в которой пропозициональные константы могут рассматриваться как представляющие определенные простые выражения вроде "Сократ — мужчина" и "Сократ смертен". Строчные литеры р, 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==ф) Эквивалентно (UU). Читается "U эквивалентно ф".
В конъюнктивной нормальной форме исчисления высказываний константы "импликация" и "эквивалентность" заменяются константами "отрицание" и "дизъюнкция", а затем отрицание сложного выражения раскрывается с помощью формул Де Моргана:
¬(U^ф) преобразуется в (¬Uv¬ф), ¬(U v ф) преобразуется в (-U^ф) , ¬¬U преобразуется в U .
Последний этап преобразований — внесение дизъюнкций внутрь скобок: (£ v (U ^ф))) заменяется ((£vU\(U)^(£vф)).
Принято сокращать вложенность скобочных форм, отбрасывая в нормальной конъюнктивной форме знаки операций v и л. Ниже представлен пример преобразования выражения, содержащего импликацию двух скобочных форм, в нормальную конъюнктивную форму.
¬(pvq)
¬¬(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 — условия, объединенные операторами конъюнкции.
Исчисление предикатов
8.1.2. Исчисление предикатов
Исчисление высказываний имеет определенные ограничения. Оно не позволяет оперировать с обобщенными утверждениями вроде "Все люди смертны". Конечно, можно обозначить такое утверждение некоторой пропозициональной константой р, а другой константой 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) Снова переименовать переменные, чтобы одни и те же имена не встречались в разных фразах.
Формальные языки
8.1. Формальные языки
Математическая логика является формальным языком в том смысле, что в отношении любой последовательности символов она позволяет сказать, удовлетворяет ли эта последовательность правилам конструирования выражений в этом языке (формулам). Обычно формальным языкам противопоставляются естественные, такие как французский и английский, в которых грамматические правила не являются жесткими. Утверждение, что логика является исчислением с определенными синтаксическими правилами логического вывода, означает, что влияние одних членов выражения на другие зависит только от формы выражения в данном языке и ни коим образом не зависит от каких-либо посторонних идей или интуитивных предположений.
Под автоматическим формированием суждений (automated reasoning) понимается поведение некоторой компьютерной программы, которая строит логический вывод на основании определенных законов. Так, нельзя отнести к классу программ автоматического формирования суждений программу, которая моделирует подбрасывание монетки, чтобы определить, следует ли одна формула из набора других. (В литературе также часто встречается термин автоматическая дедукция (automated deduction), равнозначный по смыслу термину автоматическое формирование суждений.)
При реализации автоматического формирования суждений, как правило, стремятся к максимально возможному единообразию и стандартизации в представлении формул, но в то же время в литературе часто приходится сталкиваться с самыми разнообразными системами обозначений, относящихся к логике. Основными синтаксическими схемами представления выражений являются конъюнктивная нормальная форма (conjunctive normal form— CNF), полная фразовая форма (full clausal form) и фраза Хорна (Horn clause), последняя является подмножеством полной фразовой формы. Далее мы увидим, что эти формы представления значительно упрощают процедуру логического вывода, но сначала рассмотрим некоторые вопросы исчисления высказываний и предикатов.
Язык PROLOG
8.2. Язык PROLOG
Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна представляется выражением
В языке PROLOG эта же фраза записывается в таком виде (обратите внимание на символ точки в конце):
р :- q1,...,qn. Такая фраза интерпретируется следующим образом:
"Для всех значений переменных в фразе p истинно, если истинны q1 и ... и qn",
т.е. пара символов ":-" читается как "если", а запятые читаются как "и".
PROLOG — это не совсем обычный язык программирования, в котором программа состоит в основном из логических формул, а процесс выполнения программы представляет собой доказательство теоремы определенного вида.
Фраза в форме
р :- q1, ...,qn.
Принцип резолюций
8.3.1. Принцип резолюций
Ранее я уже вскользь упоминал о том, что мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины.или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).
Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ — пропозициональные переменные, как и раньше.
Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и
U={ U1, ..., Ui, ...., Um},
и
ф= {ф1..., фi.....,фn}, и
Ui, = ¬фi при 1[i[mm,1 [j [ n,
U' = U¬{ Ui} и ф' = ф¬{ф,}.
Мощность резолюции обеспечивается тем, что в ней суммируется множество других правил. Это станет очевидно после того, как обычные правила будут представлены в конъюнктивной нормальной форме.
В левой колонке табл. 8.1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции!
Поиск доказательства в системе резолюций
8.3.2. Поиск доказательства в системе резолюций
Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорилось о том, как выполнить доказательство. В этом разделе мы обратим основное внимание на стратегические аспекты доказательства теорем.
Пусть р представляет утверждение "Сократ — это человек", a q — утверждение "Сократ смертен". Пусть наша теория имеет вид
Т={{¬р,q}, {р}}.
Таким образом, утверждается, что если Сократ человек, то Сократ смертен, и что Сократ — человек. {17} выводится из теории Т за один шаг резолюции, эквивалентной правилу modus ponens. .
Выражения {¬р, q} и {р} "сталкиваются" на паре дополняющих литералов р и ¬р, а {q} является резольвентой. Таким образом, теория Алогически подразумевает д, что записывается в форме Т|-q. Теперь можно добавить новую фразу {q} — резольвенту — в теорию Т и получить таким образом теорию
Т'= {{ ¬ip, q}, {p}, {q}}.
В этой теории р и q сохраняют прежний смысл, а г представляет утверждение "Сократ — бог". Для того чтобы показать, что Т|- ¬r , потребуются два шага резолюции:
{¬q,p},{Р}/{q}
{¬q,-r},{q} / {-r}
{¬p,q},{¬q,¬r}/{¬p,¬r},
{¬p,¬r},{p}/{¬r}
Когда множество Т велико, естественно предположить, что должно существовать несколько способов вывести интересующую нас конкретную формулу (эта формула является целевой). Естественно, что предпочтение следует отдать тому методу, который позволяет быстрее сформулировать доказательство.
Множество Т может поддерживать и те правила, которые не имеют ничего общего с доказательством целевой формулы. Как же заранее узнать, какие правила приведут нас к цели?
Потенциально весь процесс подвержен опасности комбинаторного взрыва. На каждом шаге множество Г растет, и в нашем распоряжении оказывается все больше и больше возможных путей продолжения процесса, причем некоторые из них могут привести в зацикливанию.
Та схема логического вывода, которой мы следовали до сих пор, обычно называется прямой, или восходящей стратегией. Мы начинаем с того, что нам известно, и строим логические суждения в направлении к тому, что пытаемся доказать. Один из возможных способов преодоления сформулированных выше проблем — попытаться действовать в обратном направлении: от сформулированной целевой формулы к фактам, которые нужны нам для доказательства истинности этой формулы.
Предположим, перед нами стоит задача вывести {q} из некоторого множества фраз
Т= {...,{ ¬p, q},...}.
Создается впечатление, что это множество нужно преобразовать, отыскивая фразы, включающие q в качестве литерала, а затем попытаться устранить другие литералы, если таковые найдутся. Но фраза {q} не "сталкивается" с такой фразой, как, например, { —р, q}, поскольку пара, состоящая из одинаковых литералов q, не является взаимно дополняющей.
Если q является целью, то метод опровержения резолюции реализуется добавлением негативной формулы цели к множеству Т, а затем нужно показать, что формула
Т' = Т U {¬q}
является несовместной. Полагая, что множество Т непротиворечиво, приходим к выводу, что Т' может быть противоречивым вследствие Т |- q.
В Т не существует фразы, содержащей q. В этом случае доказать искомое невозможно.
Множество Т содержит {q}. В этом случае доказательство выполняется немедленно, поскольку из {¬q} и {q} можно вывести пустую фразу, что означает несовместность (наличие противоречия).
Множество Т содержит фразу {..., q, ...}. Резольвирование этой фразы с {¬q} формирует новую фразу, которая содержит остальные литералы, причем для доказательства противоречия все они должны быть удалены в процессе резольвирования.
Эти оставшиеся литералы можно рассматривать в качестве подцелей, которые должны быть разрешены, если требуется достичь главной цели. Описанная стратегия получила название нисходящей (или обратной) и очень напоминает формулирование подцелей в системе MYCIN.
В качестве примера положим, что множество Т, как и ранее, имеет вид {{¬p,q},{¬q,¬r},{p}}. Мы пытаемся показать, что Т|- ¬r. Для этого докажем, что фраза {r} является следствием существующего множества Т, для чего добавим к этому множеству отрицание фразы ¬r. Поиск противоречия происходит следующим образом:
[{¬q,¬r},{r}]/{¬q}
[{¬p,q},{¬q}]/{¬q}
[{¬p},{p}]/{}
Теперь вернемся к примеру PROLOG-программы, представленному в листинге 8.1. На рис. 8.1 показано дерево доказательства утверждения above(a, с). Дерево строится сверху вниз, и каждая ветвь связывает две "родительские фразы", в которых содержатся дополняющие литералы, с фразой, которая образуется в результате применения правила резолюции. Ко всем целям, записанным справа от значка ":-", неявно применяется отрицание. В левой части дерева представлены формулы целей, а в правой — фразы, взятые из базы данных.
Корнем дерева является пустая фраза {}. Это означает, что поиск доказательства был успешным. Добавление негативной фразы :- above (а, с) к исходному множеству (теории) привело к противоречию. Таким образом, можно утверждать, что фраза above (а, с) является логическим следствием из этой теории.
Обратите внимание на роль операции унификации в этом доказательстве. Цель above (а, с) унифицируется с головной фразой above(X, Y) с помощью подстановки {Х/а, Y/c}, где выражение Х/а можно интерпретировать как "X получает значение а". Затем эта подстановка применяется к хвостовой части фразы
on(Z, Y), above(X, Z),
из чего следует формулировка подцелей
on(Z, с), above(a, Z).
Опровержение резолюций
8.3. Опровержение резолюций
В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation). Полное описание этого метода читатель найдет в книге Робинсона [Robinson, 1979], а в этом разделе мы попытаемся кратко изложить только основные идеи.
Процедурная дедукция в системе PLANNER
8.4. Процедурная дедукция в системе PLANNER
Система PLANNER явилась одной из первых попыток разработки языка программирования задач искусственного интеллекта, базирующегося на идеях автоматического доказательства теорем. Хотя разработчикам и не удалось в полной мере реализовать задуманное, созданное подмножество языка, получившего название Micro-PLANNER, нашло применение в системах планирования, в частности в программе SHRDLU, представленной в главе 2. Ниже мы обсудим те аспекты системы PLANNER, которые имеют отношение к представлению знаний.
Система PLANNER моделировала состояние некоторой области рассуждений в терминах ассоциативной базы данных, которая содержала как утверждения, так и теоремы, функционирующие как процедуры. Утверждения представляли собой списки типа "предикат-аргумент", подобные тем, что используются в LISP. Например:
(BLOCK B1) (ON Bl TABLE)
(ANTE (BLOCK X) (ASSERT (ON X TABLE)))
Выше был приведен пример антецедентной теоремы. Это название акцентирует внимание на том, что нас интересует только логическая связь между антецедентом и консек-вентом (по аналогии с правилом modus ponens), а не связь между отрицанием консеквен-та и отрицанием антецедента (по аналогии с правилом modus fallens). Мы говорим, что в действительности эта теорема является процедурой, поскольку в ней содержится управляющая информация. Ее функционирование во многом напоминает демонов в системе фреймов, описанных в главе 6.
Система PLANNER поддерживает и другой вид процедур, которые получили наименование консеквентной теоремы. Пример процедуры такого типа приведен ниже:
(CONSE (MORTAL X) (GOAL (MAN X))).
Консеквентные теоремы могут также манипулировать базой данных. Например, для того чтобы положить блок В1, на котором ничего не стоит, на блок В2, на котором также ничего не стоит, нужно отыскать, на чем же стоит блок В1, удалить соответствующее утверждение и сформировать новое, которое говорит, что блок В1 стоит на блоке В2.
(CONSE (ON X Y)
(GOAL (CLEAR X)) (GOAL (CLEAR Y))
(ERASE (ON X Z)) (ASSERT (ON X Y)))
Из этого краткого описания читатель может сделать заключение, что в системе PLANNER управляющая информация явно представлена в базе данных процедур, а не скрывается в компоненте, ведающем стратегией выполнения доказательства теорем, как это делается в системах, работающих на основе метода опровержения резолюций. Достоинство такого подхода состоит в том, что можно решить в каждом конкретном случае, какие правила влияния следует применять. Кроме того, в нашем распоряжении оказывается довольно эффективный инструмент моделирования изменения состояния задачи.
С концепцией процедурной дедукции связана проблема полноты. Система доказательства является полной, если все тавтологии, т.е. тривиально истинные выражения вроде (р v —pi), могут быть выведены в ней как теоремы. В системе PLANNER это свойство отсутствует. Мы уже обращали внимание на то, что нельзя сформировать выражение (MORTAL SOCRATES) из базы данных, в которой содержатся
(MAN SOCRATES)
(CONSE (MORTAL X)
(GOAL (MAN X))).
В следующем разделе мы кратко остановимся на системах, в которых была предпринята попытка устранить эти недостатки.
Правила поиска в языке PROLOG
8.5.1. Правила поиска в языке PROLOG
Существует аналогия между выражениями вида
admire(Y, X) :- philosopher (X) , beats (X,Y)
:- admire(V, W). ,
Цель, которая унифицируется с выражением admire(Y, X), может быть истолкована как вызов процедуры, а процесс унификации может рассматриваться как механизм передачи действительных параметров другим литералам, образующим тело процедуры. В данном случае не имеет значения, являются ли эти "параметры" переменными, как в представленном примере. Подцели в теле процедуры упорядочены. В языке PROLOG такое упорядочение называется правилом поиска слева направо.
В PLANNER и ранних системах, основанных на методе резолюций, цель легко достигается, если в базе данных содержатся утверждения
philosopher (zeno) . beats (zeno, achilles).
admire (achilles, zeno).
philosopher ( socrates ) .
В этом случае, если эта формула отыщется прежде, чем формула
philosopher(zeno).,
Предположим, что в базе данных содержатся факты еще о ста философах, т.е. в ней имеются сто других выражений в формате philosopher(X), в которых X отличается от zeno. Тогда в худшем случае программе потребуется 100 раз выполнить обратный просмотр, прежде чем будет найдено именно то утверждение, которое согласуется с целью.
База данных может содержать и другие правила, которые взаимодействуют с интересующим нас выражением admire (V, W). Например, можно положить, что утверждение "X обогнал Y" представляет транзитивное отношение. В этом случае в нашем распоряжении будет правило
beats(X, Y) :- beats(X, Z), beatsf Z, Y).
philosopher(X) :- beats(Y, X), tortoise(Y).
В следующем разделе описано одно из расширений языка PROLOG— система MBASE, на базе которой реализована программа МЕСНО для решения задач вузовского курса теоретической механики.
Управление поиском в системе MBASE
8.5.2. Управление поиском в системе MBASE
Один из распространенных способов управления поиском в применении к доказательству какого-либо утверждения — тщательное упорядочение базы данных. При поиске нужных фактов или правил исполнительная система языка PROLOG просматривает базу данных от начала до конца. Используя это обстоятельство, можно несколько сократить время доказательства.
Определенные факты (основные атомы — ground atoms) нужно разместить в базе данных раньше, чем правила, которые в качестве цели имеют соответствующие предикаты. Таким образом будут минимизированы издержки обращения к правилам. Например, утверждение
beats(achilles, zeno).
beats(X, Y) :- beats(X, Z), beats( Z, Y).
flies(X) :- penguin(X), !, fail .
flies(X) :- bird(X).
Предположения по умолчанию реализуются включением неосновных атомов в самый конец базы знаний. Например, если желательно, чтобы по умолчанию квакеры считались пацифистами, то фраза
pacifist(X) :- quaker(X).
pacifist(nixon) :- !, fail.
Общее правило гласит, что сначала в базе данных следует располагать данные об особых случаях, т.е. определенные факты и исключения, затем данные об общих случаях, например правила влияния, и последними должны располагаться сведения о свойствах по умолчанию.
Все эти требования соблюдены в системе MBASE, но, кроме того, еще существует и возможность управления глубиной поиска. В этой системе существуют литералы, задающие один из трех имеющихся режимов поиска.
Обращение к базе данных (DBC — database call). Этот режим ограничивает зону поиска только основными литералами в базе данных и таким образом исключает применение правил. Для настройки этого режима нужно включить основной литерал в предикат ВВС. Например, факт, что b1 является блоком, будет представлен фразой
DBC(block(b1)).
Описанная выше комбинация литералов отсечения и неудачи также может использоваться в сочетании с предикатом DBC. Таким образом, формируется своего рода "ловушка", прекращающая поиск цели, которая не может быть найдена. Например, можно таким способом прекратить попытки доказать, что блок одновременно находится в двух местах:
at(Block, Placel) :-
DEC(at(Block, Place2)), different(Placel, Place2), !, fail.
Вызов правил влияния (DBINF — inference call) — это обычный режим работы исполнительной системы PROLOG с использованием всех имеющихся правил. При этом соблюдаются соглашения о порядке поиска в базе сверху вниз, а в правиле слева направо.
Порождающий вызов (СС — creative call). В этом режиме формируются место-держатели для неизвестных и выполняются вычисления в тех случаях, когда обычный режим может привести к неудаче. Режим используется для математических вычислений, когда отсутствуют значения всех переменных в уравнении.
С помощью литералов 1 и fail обычно определяется отрицание определенной процедуры, например, так:
not(P) :- call(P) !, fail. not(P) .
Некоторые из проблем полноты, отмеченные в системе PLANNER, существуют и в языке PROLOG. В частности, использование литералов отсечения и неудачи может серьезно сказаться на полноте и согласованности фактов и правил. Существует множество способов внедрения отрицаний в логику фразы Хорна, но условия, при которых это можно сделать, весьма ограничены (см., например, [Shepherdson, 1984], [Shepherdson, 1985]).
Тем не менее исследователи пришли к выводу, что описанный выше механизм управления далеко не всегда может привести процесс вычислений к искомому заключению, поскольку не обладает достаточной "глобальностью". Проблема состоит в том, что все описанные методы базируются все-таки на довольно ограниченных, локальных знаниях о текущем состоянии процесса вычислений. В MBASE была предпринята попытка дополнить локальное управление двумя механизмами— схематизацией (schemata) и мета-предикатами. О них-то и пойдет речь ниже.
Под схематизацией подразумеваются ассоциативные механизмы, которые используются в основном для представления в компьютере знаний общего характера. Например, ниже приведено представление знаний о системе подъема грузов на основе ворота (pulley system):
sysinfo(pullsys,
[Pull, Str, P1, P2],
[pulley, string, solid, solid]
[ supports(Pull, Str),
attached(Str, Pi),
attached(Str, P2) ]).
первый аргумент, pullsys, свидетельствует о том, что эта схема представляет типовую систему подъема грузов с воротом и, таким образом, аналогичен слоту наименования;
второй аргумент, [Pull, Str, P1, P2], является перечнем деталей в этом механизме — ворот, трос и два груза;
третий аргумент, [pulley, string, solid, solid], содержит информацию о типе этих компонентов;
четвертый аргумент содержит список отношений (связей) между компонентами.
Обратите внимание на то, что в этом представлении нет никакой пропозиционально-сти, например сведений о том, каким способом можно неявно сопоставить два списка. По существу, это представление очень похоже на описание фрейма (но вряд ли с ним можно работать так же эффективно).
Описанная схематизация представляет только один из использованных в МЕСНО способов организации фоновой информации, которая нужна программе. Имеются и другие типы структур, которые помогают выбрать подходящие формулы для определения характеристических параметров той или иной моделируемой системы. Например, выражение
kind(al, accel, relaccel(...)).
relates(accel, [resolve, constaccel, relaccel)).
Роль метапредикатов состоит в отборе правил, наиболее подходящих для вывода конкретной цели. Рассмотрим следующий пример:
solve(U, Exprl, Ans) :-
occur)U, Exprl, 2), collect(U, Exprl, Expr2), isolate(U, Expr2, Ans).
в выражение Exprl неизвестная U входит дважды:
выражение Ехрг2 представляет собой Exprl, в котором выполнено приведение неизвестной U;
Ans является выражением Ехрг2, в котором неизвестная U вынесена в левую часть.
В данном случае метапредикат solve указывает способ преобразования уравнения к виду, который позволит разрешить его относительно неизвестного. Метапредикаты используются для того, чтобы формировать суждения о том, как формировать суждения, и в этом подобны метаправилам в продукционных системах.
Некоторые примеры использования системы МЕСНО демонстрируют, что методика логического программирования во многом сходна с программированием на обычных языках. Однако при создании приложений, которые требуют обработки обширного набора структурированных фактов, подчиняющихся определенным физическим законам (анализ электрических цепей или сложных механических систем), единственным подходящим языком часто оказывается PROLOG. Этот же язык может быть использован и для описания теорий, затрагивающих такие общие категории, как пространство, время, допустимость и обязательность, в которых существуют общие принципы, допускающие декларативное представление, и в которых не требуется глубокий поиск.
В главе 23 мы увидим, что, несмотря на существование определенных проблем при использовании концепций логического программирования и основанного на них языка PROLOG, эта концепция имеет приложение в двух других областях исследований, которые представляют интерес с точки зрения экспертных систем, а именно: обобщение на базе объяснения (explanation-based generalization) и логический вывод на метауровне (meta-level inference). Обобщение на базе объяснения используется для машинного обучения, а логический вывод на метауровне позволяет программе строить суждения о собственном поведении.
PROLOG и MBASE
8.5. PROLOG и MBASE
Ранее мы уже видели, что фразу, содержащую предположение, можно представить с помощью исчисления предикатов первого порядка. Фраза
"Если философ выиграет у кого-нибудь в забеге, то этот человек будет им восхищен" в формализме предикатов приобретет вид формулы
(любой A) (любой Y)(PHILOSOPHER(X)^BEATS(X, Y)
{ADMIRE(Y, X), -ВЕАТS(Х, Y), ->PHILOSOPHER(X)}.
Также было показано, что если записать это выражение таким образом, чтобы слева от оператора ":-" стоял единственный позитивный литерал, а справа — негативные литералы, то получится выражение, представляющее фразу Хорна в синтаксисе языка логического программирования PROLOG:
admire (Y, X) :- philosopher ( X) , beats (X,Y).
Ниже мы рассмотрим, как организовать управление применением таких правил.
Дерево доказательства методом опровержения резолюций
Дерево доказательства методом опровержения резолюций
Восходящий процесс доказательства, использующий в качестве отправной точки утверждение, которое мы стараемся доказать, позволяет сфокусировать внимание на процессе поиска решения, поскольку анализируемые логические связи по крайней мере потенциально ведут нас к цели. Правда, основанный на этой стратегии метод опровержения резолюций не позволяет решить все перечисленные выше проблемы. В частности, этот метод не гарантирует, что найденный путь доказательства будет короче других (или длиннее).
В следующих двух разделах мы рассмотрим эволюцию процедурных дедуктивных систем, т.е. систем, в которых процедуры используются для добавления дополнительных управляющих свойств в процесс целенаправленного поиска и для представления знаний, которые не имеют четко выраженного декларативного характера.
Процесс становления этого класса систем весьма поучителен, поскольку демонстрирует, как, отталкиваясь от стандартной логики и добавляя методики, обычно используемые при доказательстве теорем, можно построить успешно функционирующую автоматическую систему доказательства.
Логическое программирование
ГЛАВА 8. Логическое программирование 8.1. Формальные языки 8.1.1. Исчисление высказываний 8.1.2. Исчисление предикатов 8.2. Язык PROLOG 8.3. Опровержение резолюций 8.3.1. Принцип резолюций 8.3.2. Поиск доказательства в системе резолюций 8.4. Процедурная дедукция в системе PLANNER 8.5. PROLOG и MBASE 8.5.1. Правила поиска в языке PROLOG 8.5.2. Управление поиском в системе MBASE Рекомендуемая литература Упражнения
Простая программа на языке PROLOG, определяющая отношение on (на)
Листинг 8.1. Простая программа на языке PROLOG, определяющая отношение on (на)
on(а, b).
on(b, с).
above(X, Y) :- on(X, Y).
above(X, Y) :- on(Z, Y),
above(X, Z).
Литерал цели сопоставляется с литералом р (унифицируется с р), который называется головой фразы.
(1) Литерал цели сопоставляется с литералом р (унифицируется с р), который называется головой фразы.
(2)Хвост фразы ql, ...,qn конкретизируется подстановкой значений переменных (или унификаторов), сформированных в результате этого сопоставления.
(3) Конкретизированные термы хвостовой части образуют затем множество подцелей, которые могут быть использованы другими процедурами.
Таким образом, сопоставление (или унификация) играет ту же роль, что и передача параметров функции в других, более привычных языках программирования.
Логическое программирование
Логическое программирование
8.1. Формальные языки
8.2. Язык PROLOG
8.3. Опровержение резолюций
8.4. Процедурная дедукция в системе PLANNER
8.5. PROLOG и MBASE
Рекомендуемая литература
Упражнения
Еще в конце 1970-х годов стала отчетливо просматриваться тенденция к использованию в исследованиях в области искусственного интеллекта "формальных" методов, т.е. основанных на аппарате математической логики. Эти методы противопоставлялись более интуитивным и менее формализованным эвристическим методам, скажем, таким, которые были использованы в системе MYCIN. Для того чтобы стало ясно, что все это значит, нужно познакомить вас с логическими языками, а затем показать, как соотносятся их свойства с теми методами рассуждений, которые должны поддерживать типовые экспертные системы.
Рекомендуемая литература
Рекомендуемая литература
Четкое изложение основных концепций теории доказательств в математической логике читатель найдет в работе Эндрюса [Andrews, 1986]. Я также рекомендую познакомиться с книгой [Quine, 1979] — переизданием классического труда, опубликованного впервые еще в 1940 году. Достаточно обширное введение в проблематику автоматического формирования суждений содержится в книге Робинсона [Robinson, 1979].
Более популярное изложение этого материала с упором на проблематику искусственного интеллекта можно найти в работе [Genesereth andNilsson, 1987, Chapters 1-5]. Обсуждение проблем математической логики в контексте искусственного интеллекта содержится в статье Хейеса и Мичи [Hayes and Michie, 1984]. Новой работой в этой области является книга Гинзберга [Ginsberg, 1993].
Снова о роботах и комнатах
В главе 3 мы уже упоминали об исчислении предикатов в упрощенном виде. Там выражение вида
at(робот, комнатаА)
означало, что робот находится в комнате А. Термы робот и комнатаА в этом выражении представляли собой константы, которые описывали определенные реальные объекты. Но что будет означать выражение вида
at(X, комнатаА) ,
в котором х является переменной? Означает ли оно, что нечто находится в комнате А? Если это так, то говорят, что переменная имеет экзистенциальную подстановку (импорт). А может быть, выражение означает, что все объекты находятся в комнате А? В таком случае переменная имеет универсальную подстановку. Таким образом, отсутствие набора четких правил не позволяет однозначно интерпретировать приведенную формулу.
Перечисленные в этом разделе правила исчисления предикатов обеспечивают однозначную интерпретацию выражений, содержащих переменные.
В частности, фраза
at(X, комнатаА )<—at (X, ящик1) интерпретируется как
"для всех X X находится в комнате А, если X находится в ящике 1". В этой фразе переменная имеет универсальную подстановку. Аналогично, фраза
at(X, комнатаА) <-интерпретируется как "для всех X X находится в комнате А". А вот фраза
<— at(X, комнатаА) интерпретируется как "для всех XX не находится в комнате А".
Иными словами, это не тот случай, когда некоторый объект X находится в комнате А и, следовательно, переменная имеет экзистенциальную подстановку.
P1, ..., Рт <— q1,...qn содержит переменные х1,..., хk, то правильная интерпретация имеет следующий вид:
для всех x1, ..., хk
p1 или ... или pm является истинным, если q1 и ... и qn являются истинными.
Если п = 0, т.е. отсутствует хотя бы одно условие, то выражение будет интерпретироваться следующим образом:
для всех x1, ..., xk
p1 или ... или рт является истинным.
Если т = 0, т.е. отсутствуют термы заключения, то выражение будет интерпретироваться следующим образом:
для всех x1, ..., xk
не имеет значения, что q1 и ... и qn являются истинными.
Если же т = п = 0, то мы имеем дело с пустой фразой, которая всегда интерпретируется как ложная.
Обобщение резолюции
Таблица 8.1. Обобщение резолюции
Правило вывода |
Обычная форма |
Конъюнктивная нормальная форма |
||
Modus ponens |
(U |
{¬U,Ф},{U}/{ф} |
||
Modus fallens |
(U |
{¬U,ф},{-,ф}/{-U} |
||
Сцепление |
(U£)(U |
{¬U,ф},{¬ф,£}/{¬U,£} |
||
Слияние |
(U ф)/ф |
{U,ф},{¬U,ф}/{ф} |
||
Reductio |
(U,¬U)/ | |
{¬U},{U}/{} |
Главное, что нужно вынести из всего сказанного выше, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.
В исчислении предикатов использование резолюций требует дополнительных усилий, поскольку в этом исчислении присутствуют переменные. Основная операция сопоставления в доказательстве теорем с помощью резолюций называется унификацией (подробное описание используемого при этом алгоритма читатель найдет, например, в работе Нильсона [Nilsson, 1980]). При сопоставлении дополняющих литералов отыскивается такая подстановка переменных, которая превращает оба выражения в идентичные.
Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.
с помощью логики предикатов следующие
Упражнения
1. Выразите с помощью логики предикатов следующие утверждения.
I) Каждый студент использует какой-нибудь компьютер, и по крайней мере один компьютер используется каждым студентом. (Используйте только предикаты СТУДЕНТ, КОМПЬЮТЕР и ИСПОЛЬЗУЕТ.)
II) Каждый год некоторые студенты-мужчины проваливают каждый экзамен, но каждый студент-женщина сдает какой-нибудь экзамен. (Используйте только предикаты СТУДЕНТ, МУЖЧИНА, ЖЕНЩИНА, СДАЕТ, ЭКЗАМЕН, ГОД.)
Ill) Каждый мужчина любит какую-нибудь женщину, которая любит другого мужчину. (Используйте только предикаты МУЖЧИНА, ЖЕНЩИНА, ЛЮБИТ и = .)
IV) Не существует двух философов, которые любили бы одну и ту же книгу. (Используйте только предикаты ФИЛОСОФ, КНИГА, ЛЮБИТ и = .)
2. Выразите предложения упр. 1 в форме фразы.
3. Имеет ли смысл выразить следующие цитаты с помощью логики предикатов? Покажите, в чем состоит сложность такого преобразования в каждом конкретном случае.
I) Ни один человек не является островом. (Джон Донн (John Donne))
II) Человек, который живет где-нибудь, живет везде. (Тацит)
III) Прошлое — это иная страна. В нем все происходит по-другому. (Л. П. Хартли (L. P. Hartley))
4. Следующая формула утверждает, что кто-то бреет себя сам или парикмахер бреет кого-то:
бреет) X, X), бреет (парикмахер, X) <—
I) Используя обратную стратегию, покажите, что из этой формулы следует
бреет (парикмахер, парикмахер) <-
II) То же самое покажите с помощью прямой стратегии.
III) Как вы понимаете в том же контексте следующую фразу:
<- бреет(У, Y), бреет (парикмахер, У)
IV) Покажите, что следующие фразы противоречивы. Для этого достаточно показать, что из них следует пустая фраза:
бреет(Х, X), бреет (парикмахер, X)
<-<- бреет(У, Y), бреет (парикмахер, Y)
5. Ниже представлены правило поиска неисправности и описание конкретной ситуации.
Если компьютер не включается и напряжение в сети питания в норме, то оборван шнур питания или неисправен блок питания. Мой компьютер не включается. Напряжение в сети питания в норме. Шнур питания не оборван.
I) Выразите эти предложения в форме логики предикатов.
II) Постройте конъюнктивную нормальную форму.
III) Используя прямую стратегию доказательства, покажите, что утверждение "Неисправен блок питания" логически вытекает из приведенного набора фактов. То же самое покажите с использованием обратной стратегии доказательства.
6. Предположим, что в синтаксисе языка PROLOG цель сформулирована следующим образом :- bachelor (f red).
I) К какому заключению придет приведенная ниже PROLOG-программа относительно семейного положения человека по имени Fred?
man(fred).
man(george).
wife(george, georgina).
bachelor(X) :- not(wife(X, Y)).
not(P) :- call(P), !, fail.
not(P).
II) К какому заключению придет приведенная ниже PROLOG-программа?
man(fred).
man(george).
wife(george, georgina).
bachelor(X) :- not(wife(X, Y)).
(wife(X, Y) :- !, fail.
(wifeffred, freda).
7. Предположим, что в синтаксисе языка PROLOG цель сформулирована следующим образом :- enemy(fred).
I) К какому заключению придет приведенная ниже MBASE-программа относительно человека по имени Fred?
DBC(friend (george)).
republican(fred).
enemy(X) :- not(DBC(friend(X))).
friend(X)) :- republican(X).
not(P) :- call(P), !, fail.
not(P).
II) К какому заключению придет приведенная ниже MBASE-программа?
DBC(friend (george)).
enemy(X) :- not(DBC(friend(X))). friend(X))
:- not(communist(X)). not(P)
:- call(P), !, fail. not(P).
8. Ниже приведена программа на языке PROLOG, в которой идентифицируется подмножество лиц, имеющих право работать в службе обеспечения общественного порядка штата Нью-Йорк. Вы можете ввести эту программу в исполнительную систему PROLOG и поэкспериментировать с ней.
Затем попробуйте добавить в программу новое правило, касающееся еще одной категории служащих.
Деревенские констебли, назначенные с условием, что это не противоречит законам штата.
Данные для тестирования этого правила включены в раздел фактов программы.
/ Правила для сотрудников службы общественного порядка /
/ Шериф и заместитель шерифа округа Нью-Йорк /
/ The sheriff and deputy sheriff of NYC /
po(X) :-
(sheriff(X) ; deputy(X)), jurisdiction(X, nyc).
/ Сотрудники службы охраны порядка
округа Уэстчестер, принятые на
работу после 1982 года, которые
выполняют функции, ранее возлагавшиеся
на шерифа округа Уэстчестер /
/ Officers of Westchester country
public safety services appointed
after 1982 who perform functions
previously performed by a Westchester
country sheriff on or prior to such date /
po(X) :-
safetyOfficer(X), jurisdiction(X, Westchester),
appointed(X, Date), Date > 1982.
/ ФАКТЫ /
/ Wayne, Doug, Ken и Pete - некоторые лица. /.
sheriff(wayne).
jurisdiction(wayne, nyc).
deputy(doug), jurisdictionfdoug, nyc).
constable(ken), jurisdiction(ken, naples).
village(naples). RuledOut(constable, naples).
safetyOfficer(pete) jurisdiction(pete, Westchester).
appointed(pete, 1990).
9. Запишите программу из упр. 8 на языке CLIPS. Сравните оба варианта программы.