Формальные языки
Математическая логика является формальным языком в том смысле, что в отношении любой последовательности символов она позволяет сказать, удовлетворяет ли эта последовательность правилам конструирования выражений в этом языке (формулам). Обычно формальным языкам противопоставляются естественные, такие как французский и английский, в которых грамматические правила не являются жесткими. Утверждение, что логика является исчислением с определенными синтаксическими правилами логического вывода, означает, что влияние одних членов выражения на другие зависит только от формы выражения в данном языке и ни коим образом не зависит от каких-либо посторонних идей или интуитивных предположений.
Под автоматическим формированием суждений (automated reasoning) понимается поведение некоторой компьютерной программы, которая строит логический вывод на основании определенных законов. Так, нельзя отнести к классу программ автоматического формирования суждений программу, которая моделирует подбрасывание монетки, чтобы определить, следует ли одна формула из набора других. (В литературе также часто встречается термин автоматическая дедукция (automated deduction), равнозначный по смыслу термину автоматическое формирование суждений.)
При реализации автоматического формирования суждений, как правило, стремятся к максимально возможному единообразию и стандартизации в представлении формул, но в то же время в литературе часто приходится сталкиваться с самыми разнообразными системами обозначений, относящихся к логике. Основными синтаксическими схемами представления выражений являются конъюнктивная нормальная форма (conjunctive normal form— CNF), полная фразовая форма (full clausal form) и фраза Хорна (Horn clause), последняя является подмножеством полной фразовой формы. Далее мы увидим, что эти формы представления значительно упрощают процедуру логического вывода, но сначала рассмотрим некоторые вопросы исчисления высказываний и предикатов.
Исчисление высказываний
Исчисление высказываний представляет собой логику неанализируемых предположений, в которой пропозициональные константы могут рассматриваться как представляющие определенные простые выражения вроде "Сократ — мужчина" и "Сократ смертен". Строчные литеры р, 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==ф) Эквивалентно (U
U).
Читается "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 — условия, объединенные операторами конъюнкции.
Исчисление предикатов
Исчисление высказываний имеет определенные ограничения. Оно не позволяет оперировать с обобщенными утверждениями вроде "Все люди смертны". Конечно, можно обозначить такое утверждение некоторой пропозициональной константой р, а другой константой 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.
Снова о роботах и комнатах
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, то мы имеем дело с пустой фразой, которая всегда интерпретируется как ложная.
Язык PROLOG
Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна представляется выражением
В языке PROLOG эта же фраза записывается в таком виде (обратите внимание на символ точки в конце):
р :- q1,...,qn. Такая фраза интерпретируется следующим образом:
"Для всех значений переменных в фразе p истинно, если истинны q1 и ... и qn",
т.е. пара символов ":-" читается как "если", а запятые читаются как "и".
PROLOG — это не совсем обычный язык программирования, в котором программа состоит в основном из логических формул, а процесс выполнения программы представляет собой доказательство теоремы определенного вида.
Фраза в форме
р :- q1, ...,qn.
может рассматриваться в качестве процедуры. Такая процедура предполагает следующий порядок выполнения операций.
(1) Литерал цели сопоставляется с литералом р (унифицируется с р), который называется головой фразы.
(2)Хвост фразы ql, ...,qn конкретизируется подстановкой значений переменных (или унификаторов), сформированных в результате этого сопоставления.
(3) Конкретизированные термы хвостовой части образуют затем множество подцелей, которые могут быть использованы другими процедурами.
Таким образом, сопоставление (или унификация) играет ту же роль, что и передача параметров функции в других, более привычных языках программирования.
Например, рассмотрим набор фраз языка PROLOG, представленных в листинге 8.1. Предположим, что a, b и с — какие-то блоки в мире блоков. Две первые фразы утверждают, что а находится на (on) b, a b находится на (on) с. Третья фраза утверждает, что X находится выше (above) Y, если X находится на (on) Y. Четвертая фраза утверждает, что X находится выше (above) Y, если существует какой-то другой блок Z, размещенный на (on) Y, и X находится выше (above) Y.
Листинг
8.1. Простая программа на языке PROLOG, определяющая отношение on (на)
on(b, с).
above(X, Y) :- on(X, Y).
above(X, Y) :- on(Z, Y), above(X, Z).
Очевидно, что от программы требуется вывести цель above (а, с) из этого множества фраз. Как это делается, мы увидим в разделе 8.3.2, но уже сейчас можно сказать, что процесс формулировки выражения цели включает обработку двух процедур above и использование двух фраз on.
Опровержение резолюций
В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation). Полное описание этого метода читатель найдет в книге Робинсона [Robinson, 1979], а в этом разделе мы попытаемся кратко изложить только основные идеи.
Принцип резолюций
Ранее я уже вскользь упоминал о том, что мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины.или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).
Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ — пропозициональные переменные, как и раньше.
Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и
U={ U1, ..., Ui, ...., Um}, и
ф= {ф1..., фi.....,фn}, и
Ui, = ¬фi при 1[i[mm,1 [j [ n,
то новую фразу £ можно вывести из объединения U' и ф', где
U' = U¬{ Ui} и ф' = ф¬{ф,}.
Фраза £ = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и фj.
Мощность резолюции обеспечивается тем, что в ней суммируется множество других правил. Это станет очевидно после того, как обычные правила будут представлены в конъюнктивной нормальной форме.
В левой колонке табл. 8.1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции!
Таблица 8.1.
Обобщение резолюции
|
Правило
вывода |
Обычная
форма |
Конъюнктивная
нормальная форма |
||
|
Modus ponens |
(U |
{¬U,Ф},{U}/{ф} |
||
|
Modus fallens |
(U |
{¬U,ф},{-,ф}/{-U} |
||
|
Сцепление |
(U |
{¬U,ф},{¬ф,£}/{¬U,£} |
||
|
Слияние |
(U |
{U,ф},{¬U,ф}/{ф} |
||
|
Reductio |
(U,¬U)/ | |
{¬U},{U}/{} |
Главное, что нужно вынести из всего сказанного выше, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.
В исчислении предикатов использование резолюций требует дополнительных усилий, поскольку в этом исчислении присутствуют переменные. Основная операция сопоставления в доказательстве теорем с помощью резолюций называется унификацией (подробное описание используемого при этом алгоритма читатель найдет, например, в работе Нильсона [Nilsson, 1980]). При сопоставлении дополняющих литералов отыскивается такая подстановка переменных, которая превращает оба выражения в идентичные.
Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.
Поиск доказательства в системе резолюцийРезолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорилось о том, как выполнить доказательство. В этом разделе мы обратим основное внимание на стратегические аспекты доказательства теорем. Пусть р представляет утверждение "Сократ — это человек", a q — утверждение "Сократ смертен". Пусть наша теория имеет вид Т={{¬р,q}, {р}}. Таким образом, утверждается, что если Сократ человек, то Сократ смертен, и что Сократ — человек. {17} выводится из теории Т за один шаг резолюции, эквивалентной правилу modus ponens. . Выражения {¬р, q} и {р} "сталкиваются" на паре дополняющих литералов р и ¬р, а {q} является резольвентой. Таким образом, теория Алогически подразумевает д, что записывается в форме Т|-q. Теперь можно добавить новую фразу {q} — резольвенту — в теорию Т и получить таким образом теорию Т'= {{ ¬ip, q}, {p}, {q}}. Конечно, в большинстве случаев для доказательства требуется множество шагов. Положим, например, что теория Т имеет вид В этой теории р и q сохраняют прежний смысл, а г представляет утверждение "Сократ — бог". Для того чтобы показать, что Т|- ¬r , потребуются два шага резолюции: {¬q,p},{Р}/{q} {¬q,-r},{q} / {-r} Обратите внимание, что на первом шаге используются две фразы из исходного множества Т, а на втором— резольвента {q}, добавленная к Т. Кроме того, следует отметить, что доказательство может быть выполнено и по-другому, например: {¬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} можно вывести пустую фразу, что означает несовместность (наличие противоречия). Множество Т содержит фразу {..., 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). Следующая подцель on(Z, с) унифицируется с on(b, с) подстановкой {Z/b}. Эта подстановка затем применяется и к оставшейся подцели, которая таким образом превращается в above (а, b), и так до тех пор, пока не образуется пустая фраза.
Рис. 8.1.
Дерево доказательства методом опровержения резолюций В следующих двух разделах мы рассмотрим эволюцию процедурных дедуктивных систем, т.е. систем, в которых процедуры используются для добавления дополнительных управляющих свойств в процесс целенаправленного поиска и для представления знаний, которые не имеют четко выраженного декларативного характера. Процесс становления этого класса систем весьма поучителен, поскольку демонстрирует, как, отталкиваясь от стандартной логики и добавляя методики, обычно используемые при доказательстве теорем, можно построить успешно функционирующую автоматическую систему доказательства. Процедурная дедукция в системе PLANNERСистема PLANNER явилась одной из первых попыток разработки языка программирования задач искусственного интеллекта, базирующегося на идеях автоматического доказательства теорем. Хотя разработчикам и не удалось в полной мере реализовать задуманное, созданное подмножество языка, получившего название Micro-PLANNER, нашло применение в системах планирования, в частности в программе SHRDLU, представленной в главе 2. Ниже мы обсудим те аспекты системы PLANNER, которые имеют отношение к представлению знаний. Система PLANNER моделировала состояние некоторой области рассуждений в терминах ассоциативной базы данных, которая содержала как утверждения, так и теоремы, функционирующие как процедуры. Утверждения представляли собой списки типа "предикат-аргумент", подобные тем, что используются в LISP. Например: (BLOCK B1) (ON Bl TABLE) Теоремы же в действительности представляли собой выражения, в которых можно было проследить влияние одних термов на другие. Например, теорема (ANTE (BLOCK X) (ASSERT (ON X TABLE))) в действительности является процедурой, которая говорит: "Если утверждается, что X это блок, то также утверждается, что X находится на столе". Таким образом, если существует утверждение (BLOCK B1), то можно также считать утверждением и выражение (ON Bl TABLE). Функция ASSERT добавляет собственный конкретизированный аргумент (т.е. аргумент, которому присвоено определенное значение) в базу данных. Выше был приведен пример антецедентной теоремы. Это название акцентирует внимание на том, что нас интересует только логическая связь между антецедентом и консек-вентом (по аналогии с правилом modus ponens), а не связь между отрицанием консеквен-та и отрицанием антецедента (по аналогии с правилом modus fallens). Мы говорим, что в действительности эта теорема является процедурой, поскольку в ней содержится управляющая информация. Ее функционирование во многом напоминает демонов в системе фреймов, описанных в главе 6. Система PLANNER поддерживает и другой вид процедур, которые получили наименование консеквентной теоремы. Пример процедуры такого типа приведен ниже: (CONSE (MORTAL X) (GOAL (MAN X))). Эта процедура может быть прочитана так: "Для того чтобы показать, что X смертен, покажите, что X — человек". Если выражение, которое нужно доказать (цель), сформулировано в виде (MORTAL SOCRATES) (Сократ смертен), то в качестве подцели будет выступать выражение (MAN SOCRATES) (Сократ человек). Функция GOAL организует поиск в базе данных собственного конкретизированного аргумента. Однако не удастся использовать эту теорему для перехода от утверждения (MAN SOCRATES) (Сократ человек) к утверждению (MORTAL SOCRATES) (Сократ смертен). Консеквентные теоремы могут также манипулировать базой данных. Например, для того чтобы положить блок В1, на котором ничего не стоит, на блок В2, на котором также ничего не стоит, нужно отыскать, на чем же стоит блок В1, удалить соответствующее утверждение и сформировать новое, которое говорит, что блок В1 стоит на блоке В2. (CONSE (ON X Y) (GOAL (CLEAR X)) (GOAL (CLEAR Y)) (ERASE (ON X Z)) (ASSERT (ON X Y))) Задавшись целью (ON Bl B2), если на Bl и на В2 ничего не стоит, PLANNER выполнит необходимые операции с базой данных. Таким образом, консеквентная теорема поддерживает в системах автоматизации планирования работу механизма реализации операторов, подобных тем, которые мы видели в программе STRIPS (см. главу 3). Из этого краткого описания читатель может сделать заключение, что в системе PLANNER управляющая информация явно представлена в базе данных процедур, а не скрывается в компоненте, ведающем стратегией выполнения доказательства теорем, как это делается в системах, работающих на основе метода опровержения резолюций. Достоинство такого подхода состоит в том, что можно решить в каждом конкретном случае, какие правила влияния следует применять. Кроме того, в нашем распоряжении оказывается довольно эффективный инструмент моделирования изменения состояния задачи. С концепцией процедурной дедукции связана проблема полноты. Система доказательства является полной, если все тавтологии, т.е. тривиально истинные выражения вроде (р v —pi), могут быть выведены в ней как теоремы. В системе PLANNER это свойство отсутствует. Мы уже обращали внимание на то, что нельзя сформировать выражение (MORTAL SOCRATES) из базы данных, в которой содержатся (MAN SOCRATES) (CONSE (MORTAL X) (GOAL (MAN X))). Это те издержки, с которыми нужно смириться, если мы хотим объединить управляющую информацию с пропозициональным представлением. К сожалению, система PLANNER оказалась не более эффективной, чем системы, основанные на теоремах резолюций. Это произошло потому, что использованная в ней управляющая информация страдает "близорукостью", отсутствует общая стратегия, а имеющийся набор теорем позволяет формулировать локальные решения, которые могут давать, а могут и не давать желаемый эффект. Отсутствует в PLANNER и возможность каким-то образом формировать суждения о механизме управления, что-то вроде метаправил, о которых шла речь в главе 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). Ниже мы рассмотрим, как организовать управление применением таких правил. Правила поиска в языке PROLOGСуществует аналогия между выражениями вида admire(Y, X) :- philosopher (X) , beats (X,Y) в языке PROLOG и консеквентной теоремой в системе PLANNER. При запросе "who admires whom?" ("кто кем восхищается?"), который может быть представлен в виде фразы :- admire(V, W). , приведенное выше выражение интерпретируется следующим образом: "Для того чтобы показать, что Y восхищается X, покажите, что X является философом, а затем покажите, что X обогнал Y". Цель, которая унифицируется с выражением admire(Y, X), может быть истолкована как вызов процедуры, а процесс унификации может рассматриваться как механизм передачи действительных параметров другим литералам, образующим тело процедуры. В данном случае не имеет значения, являются ли эти "параметры" переменными, как в представленном примере. Подцели в теле процедуры упорядочены. В языке PROLOG такое упорядочение называется правилом поиска слева направо. В PLANNER и ранних системах, основанных на методе резолюций, цель легко достигается, если в базе данных содержатся утверждения philosopher (zeno) . beats (zeno, achilles). Тогда получим ответ admire (achilles, zeno). Если в базе данных содержится другая информация, касающаяся искомой цели, то программе может потребоваться выполнить обратный просмотр (backtrack), прежде чем добраться до цели. Обратный просмотр используется в том случае, когда нужно отменить присвоение значений переменным, выполненное при обработке некоторой подцели, поскольку это присвоение приводит к неудаче в обработке поздней подцели. Положим, что база данных содержит дополнительную фразу philosopher ( socrates ) . В этом случае, если эта формула отыщется прежде, чем формула philosopher(zeno)., обработка следующей подцели приведет к неудаче, а следовательно, нужно будет поискать другого философа. Объем работы, который придется выполнить системе в процессе достижения цели admire(V, W), зависит от количества альтернативных вариантов утверждений, касающихся философов, которые имеются в базе данных. Предположим, что в базе данных содержатся факты еще о ста философах, т.е. в ней имеются сто других выражений в формате 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Один из распространенных способов управления поиском в применении к доказательству какого-либо утверждения — тщательное упорядочение базы данных. При поиске нужных фактов или правил исполнительная система языка PROLOG просматривает базу данных от начала до конца. Используя это обстоятельство, можно несколько сократить время доказательства. Определенные факты (основные атомы — ground atoms) нужно разместить в базе данных раньше, чем правила, которые в качестве цели имеют соответствующие предикаты. Таким образом будут минимизированы издержки обращения к правилам. Например, утверждение beats(achilles, zeno). должно стоять раньше правила beats(X, Y) :- beats(X, Z), beats( Z, Y). Исключения из общих правил также должны располагаться в базе данных раньше, чем сами общие правила. Например, правило, утверждающее, что пингвины не летают, flies(X) :- penguin(X), !, fail . должно стоять раньше общего правила, гласящего, что птицы летают, flies(X) :- bird(X). Литерал fail представляет собой один из способов выражения отрицания в языке PROLOG. Кроме того, в языке PROLOG имеется литерал !, который называется "отсечением". Этот литерал говорит исполнительной системе PROLOG, что не нужно осуществлять возврат из этой точки. Комбинация литералов представляет эффективный механизм управления обратным просмотром, предотвращая выполнение ненужных операций. Предположения по умолчанию реализуются включением неосновных атомов в самый конец базы знаний. Например, если желательно, чтобы по умолчанию квакеры считались пацифистами, то фраза pacifist(X) :- quaker(X). должна появиться после всех фраз вида pacifist(nixon) :- !, fail. В случае, если при просмотре базы знаний не будет найдено утверждение об обратном, касающееся конкретного квакера, то на него распространится утверждение, справедливое для всех остальных. Общее правило гласит, что сначала в базе данных следует располагать данные об особых случаях, т.е. определенные факты и исключения, затем данные об общих случаях, например правила влияния, и последними должны располагаться сведения о свойствах по умолчанию. Все эти требования соблюдены в системе MBASE, но, кроме того, еще существует и возможность управления глубиной поиска. В этой системе существуют литералы, задающие один из трех имеющихся режимов поиска. Обращение к базе данных (DBC — database call). Этот режим ограничивает зону поиска только основными литералами в базе данных и таким образом исключает применение правил. Для настройки этого режима нужно включить основной литерал в предикат ВВС. Например, факт, что b1 является блоком, будет представлен фразой DBC(block(b1)). Тогда для некоторой фразы Р при обработке подцелей в форме DBC (Р) будет просматриваться только указанная часть базы данных. Описанная выше комбинация литералов отсечения и неудачи также может использоваться в сочетании с предикатом 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) . В языке PROLOG специальный предикат call обрабатывает цель, переданную ему в качестве параметра. Идея состоит в том, что если такая обработка приведет к успеху, то отрицание цели приведет к неудаче, а литерал отсечения предотвратит обратный просмотр. В противном случае мы перейдем ко второй фразе, и отрицание цели очевидно приведет к успеху. Некоторые из проблем полноты, отмеченные в системе 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) ]). Предикат sysinfo принимает четыре аргумента, каждый из которых аналогичен слоту в системе фреймов (см. об этом в главе 6): первый аргумент, pullsys, свидетельствует о том, что эта схема представляет типовую систему подъема грузов с воротом и, таким образом, аналогичен слоту наименования; второй аргумент, [Pull, Str, P1, P2], является перечнем деталей в этом механизме — ворот, трос и два груза; третий аргумент, [pulley, string, solid, solid], содержит информацию о типе этих компонентов; четвертый аргумент содержит список отношений (связей) между компонентами. Обратите внимание на то, что в этом представлении нет никакой пропозиционально-сти, например сведений о том, каким способом можно неявно сопоставить два списка. По существу, это представление очень похоже на описание фрейма (но вряд ли с ним можно работать так же эффективно). Описанная схематизация представляет только один из использованных в МЕСНО способов организации фоновой информации, которая нужна программе. Имеются и другие типы структур, которые помогают выбрать подходящие формулы для определения характеристических параметров той или иной моделируемой системы. Например, выражение kind(al, accel, relaccel(...)). означает, что al является параметром типа accel (ускорение), который определен в утверждении relaccel, т.е. в контексте относительных ускорений. Другое выражение relates(accel, [resolve, constaccel, relaccel)). означает, что формулы resolve, constaccel и relaccel содержат переменные типа accel и, следовательно, могут быть использованы для вычисления ускорения. Приведенные выражения можно рассматривать как один из видов дополнительного индексирования в ассоциативной сети. В данном случае индексирование представлено в форме логики, причем используются структуры, обычно редко встречающиеся в исчислении предикатов первого порядка. Роль метапредикатов состоит в отборе правил, наиболее подходящих для вывода конкретной цели. Рассмотрим следующий пример: solve(U, Exprl, Ans) :- occur)U, Exprl, 2), collect(U, Exprl, Expr2), isolate(U, Expr2, Ans). Эта процедура означает, что Ans является уравнением, которое решается относительно неизвестного U в выражении Exprl, если в выражение Exprl неизвестная U входит дважды: выражение Ехрг2 представляет собой Exprl, в котором выполнено приведение неизвестной U; Ans является выражением Ехрг2, в котором неизвестная U вынесена в левую часть. В данном случае метапредикат solve указывает способ преобразования уравнения к виду, который позволит разрешить его относительно неизвестного. Метапредикаты используются для того, чтобы формировать суждения о том, как формировать суждения, и в этом подобны метаправилам в продукционных системах. Некоторые примеры использования системы МЕСНО демонстрируют, что методика логического программирования во многом сходна с программированием на обычных языках. Однако при создании приложений, которые требуют обработки обширного набора структурированных фактов, подчиняющихся определенным физическим законам (анализ электрических цепей или сложных механических систем), единственным подходящим языком часто оказывается PROLOG. Этот же язык может быть использован и для описания теорий, затрагивающих такие общие категории, как пространство, время, допустимость и обязательность, в которых существуют общие принципы, допускающие декларативное представление, и в которых не требуется глубокий поиск. В главе 23 мы увидим, что, несмотря на существование определенных проблем при использовании концепций логического программирования и основанного на них языка PROLOG, эта концепция имеет приложение в двух других областях исследований, которые представляют интерес с точки зрения экспертных систем, а именно: обобщение на базе объяснения (explanation-based generalization) и логический вывод на метауровне (meta-level inference). Обобщение на базе объяснения используется для машинного обучения, а логический вывод на метауровне позволяет программе строить суждения о собственном поведении. Рекомендуемая литератураЧеткое изложение основных концепций теории доказательств в математической логике читатель найдет в работе Эндрюса [Andrews, 1986]. Я также рекомендую познакомиться с книгой [Quine, 1979] — переизданием классического труда, опубликованного впервые еще в 1940 году. Достаточно обширное введение в проблематику автоматического формирования суждений содержится в книге Робинсона [Robinson, 1979]. Более популярное изложение этого материала с упором на проблематику искусственного интеллекта можно найти в работе [Genesereth andNilsson, 1987, Chapters 1-5]. Обсуждение проблем математической логики в контексте искусственного интеллекта содержится в статье Хейеса и Мичи [Hayes and Michie, 1984]. Новой работой в этой области является книга Гинзберга [Ginsberg, 1993].
|
