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

Содержание.

Введение………………………………….……………………………….3

1. Основные производители……………………………………………..5

2. История возникновения и развития языка ПРОЛОГ……….……….6

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

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

3.2. Программирование на ПРОЛОГЕ…………………………………14

3.3. Принцип резолюций……………………………………..…………16

3.4. Поиск доказательства в системе резолюций………………….…..18 Заключение……………………………………………………………….22

Список литературы………..…………………………………………..…24

Введение.

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

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

Среди специализированных систем, основанных на знаниях, наиболее значимы экспертные системы реального времени, или динамические экспертные системы. На их долю приходится 70 процентов этого рынка.

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

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

Коммерческие успехи к экспертным системам и нейронным сетям пришли не сразу. На протяжении ряда лет (с 1960-х годов) успехи касались в основном исследовательских разработок, демонстрировавших пригодность систем искусственного интеллекта для практического использования. Начиная примерно с 1985 (а в массовом масштабе, вероятно, с 1988-1990 годов), в первую очередь, экспертные системы, а в последние два года и нейронные сети стали активно использоваться в реальных приложениях.

1. Основные производители.

Инструментарий для создания экспертных систем реального времени впервые выпустила фирма Lisp Machine Inc в 1985 году. Этот продукт предназначался для символьных ЭВМ Symbolics и носил название Picon. Его успех привел к тому, что группа ведущих его разработчиков образовала фирму Gensym, которая, значительно развив идеи, заложенные в Picon, выпустила в 1988 году инструментальное средство под названием G2. В настоящий момент работает его третья версия и подготовлена четвертая.

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

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

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

При реализации автоматического формирования суждений, как правило, стремятся к максимально возможному единообразию и стандартизации в представлении формул, но в то же время в литературе часто приходится сталкиваться с самыми разнообразными системами обозначений, относящихся к логике. Основными синтаксическими схемами представления выражений являются конъюнктивная нормальная форма (conjunctive normal form— CNF), полная фразовая форма (full clausal form) и фраза Хорна (Horn clause), последняя является подмножеством полной фразовой формы.

2. История возникновения и развития языка ПРОЛОГ.

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

В октябре 1981 года Японское министерство международной торговли и промышленности объявило о создании исследовательской организации — Института по разработке методов создания компьютеров нового поколения (Institute for New Generation Computer Technology Research Center). Целью данного проекта было создание систем обработки информации, базирующихся на знаниях. Предполагалось, что эти системы будут обеспечивать простоту управления за счет возможности общения с пользователями при помощи естественного языка. Эти системы должны были самообучаться, использовать накапливаемые в памяти знания для решения различного рода задач, предоставлять пользователям экспертные консультации, причем от пользователя не требовалось быть специалистом в информатике. Предполагалось, что человек сможет использовать ЭВМ пятого поколения так же легко, как любые бытовые электроприборы типа телевизора, магнитофона и пылесоса. Вскоре вслед за японским стартовали американский и европейский проекты.

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

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

В качестве основной методологии разработки программных средств для проекта ЭВМ пятого поколения было избрано логическое программирование, ярким представителем которого является язык Пролог. Думается, что и в настоящее время Пролог остается наиболее популярным языком искусственного интеллекта в Японии и Европе (в США, традиционно, более распространен другой язык искусственного интеллекта - язык функционального программирования Лисп).

Название языка "Пролог" происходит от слов ЛОГическое ПРОграммирование (PROgrammation en LOGique во французском варианте и PROgramming in LOGic — в английском).

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

В истории возникновения и развития языка Пролог можно выделить следующие этапы.

В 1965 году в работе "A machine oriented logic based on the resolution principle", опубликованной в 12 номере журнала "Journal of the ACM", Дж Робинсон представил метод автоматического поиска доказательства теорем в исчислении предикатов первого порядка, получивший название "принцип резолюции". На самом деле, идея данного метода была предложена Эрбраном в 1931 году, когда еще не было компьютеров. Робинсон модифицировал этот метод так, что он стал пригоден для автоматического, компьютерного использования, и, кроме того, разработал эффективный алгоритм унификации, составляющий базис его метода.

В 1973 году "группа искусственного интеллекта" во главе с Аланом Колмероэ создала в Марсельском университете программу, предназначенную для доказательства теорем. Эта программа использовалась при построении систем обработки текстов на естественном языке. Программа доказательства теорем получила название Prolog (от Programmation en Logique). Она и послужила прообразом Пролога. Ходят легенды, что автором этого названия была жена Алана Колмероэ. Программа была написана на Фортране и работала довольно медленно.

Большое значение для развития логического программирования имела работа Роберта Ковальского "Логика предикатов как язык программирования" (Kowalski R. Predicate Logic as Programming Language. IFIP Congress, 1974), в которой он показал, что для того чтобы добиться эффективности, нужно ограничиться использованием множества хорновских дизъюнктов. Кстати, известно, что Ковальский и Колмероэ работали вместе в течение одного лета.

В 1976 г. Ковальский вместе с его коллегой Маартеном ван Эмденом предложил два подхода к прочтению текстов логических программ: процедурный и декларативный. Об этих подходах речь пойдет в третьей лекции.

В 1977 году в Эдинбурге Уоррен и Перейра создали очень эффективный компилятор языка Пролог для ЭВМ DEC–10, который послужил прототипом для многих последующих реализаций Пролога. Что интересно, компилятор был написан на самом Прологе. Эта реализация Пролога, известная как "эдинбургская версия", фактически стала первым и единственным стандартом языка. Алгоритм, использованный при его реализации, послужил прототипом для многих последующих реализаций языка. Как правило, если современная Пролог-система и не поддерживает эдинбургский Пролог, то в ее состав входит подсистема, переводящая прологовскую программу в "эдинбургский" вид. Имеется, конечно, стандарт ISO/IEC 13211– 1:1995, но его поддерживают далеко не все Прологсистемы.

В 1980 году Кларк и Маккейб в Великобритании разработали версию Пролога для персональных ЭВМ.

В 1981 году стартовал вышеупомянутый проект Института по разработке методов создания компьютеров нового поколения.

На сегодня существует довольно много реализаций Пролога. Наиболее известные из них следующие: BinProlog, AMZI-Prolog, Arity Prolog, CProlog, Micro Prolog, МПролог, Prolog-2, Quintus Prolog, SICTUS Prolog, Silogic Knowledge Workbench, Strawberry Prolog, SWI Prolog, UNSW Prolog и т. д.

В нашей стране были разработаны такие версии Пролога как Пролог-Д (Сергей Григорьев), Акторный Пролог (Алексей Морозов), а также Флэнг (А. Манцивода, Вячеслав Петухин).

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

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

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

P1, ..., Рт <— q1,...qn содержит переменные х1,..., хk, то правильная интерпретация имеет следующий вид:

для всех x1, ..., хk

p1 или ... или pm является истинным, если q1 и ... и qn являются истинными.

Если п = 0, т.е. отсутствует хотя бы одно условие, то выражение будет интерпретироваться следующим образом:

для всех x1, ..., xk

p1 или ... или рт является истинным.

Если т = 0, т.е. отсутствуют термы заключения, то выражение будет интерпретироваться следующим образом:

для всех x1, ..., xk

не имеет значения, что q1 и ... и qn являются истинными.

Если же т = п = 0, то мы имеем дело с пустой фразой, которая всегда интерпретируется как ложная.

3.2 Программирование на ПРОЛОГЕ.

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

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

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

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

Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна представляется выражением

В языке PROLOG эта же фраза записывается в таком виде:

р :- q1,...,qn. Такая фраза интерпретируется следующим образом:

"Для всех значений переменных в фразе p истинно, если истинны q1 и ... и qn",

т.е. пара символов ":-" читается как "если", а запятые читаются как "и".

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

Фраза в форме

р :- q1, ...,qn.

может рассматриваться в качестве процедуры. Такая процедура предполагает следующий порядок выполнения операций.

(1) Литерал цели сопоставляется с литералом р (унифицируется с р), который называется головой фразы.

(2)Хвост фразы ql, ...,qn конкретизируется подстановкой значений переменных (или унификаторов), сформированных в результате этого сопоставления.

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

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

Например, рассмотрим набор фраз языка PROLOG, представленных в листинге 1. Предположим, что a, b и с — какие-то блоки в мире блоков. Две первые фразы утверждают, что а находится на (on) b, a b находится на (on) с. Третья фраза утверждает, что X находится выше (above) Y, если X находится на (on) Y. Четвертая фраза утверждает, что X находится выше (above) Y, если существует какой-то другой блок Z, размещенный на (on) Y, и X находится выше (above) Y.

Листинг 1. Простая программа на языке PROLOG, определяющая отношение

on (на)

on(а, b).

on(b, с).

above(X, Y) :- on(X, Y).

above(X, Y) :- on(Z, Y),

above(X, Z).

Очевидно, что от программы требуется вывести цель above (а, с) из этого множества фраз. Процесс формулировки выражения цели включает обработку двух процедур above и использование двух фраз on. В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation).

3.3 Принцип резолюций

Мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([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.

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

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

Таблица 1. Обобщение резолюции.

	Правило вывода	Обычная форма	Конъюнктивная нормальная форма
	Modus ponens	(Uф,U)/Ф	{¬U,Ф},{U}/{ф}
	Modus fallens	(Uф.¬ф)/-U	{¬U,ф},{-,ф}/{-U}
	Сцепление	(Uф,ф£)(U£)	{¬U,ф},{¬ф,£}/{¬U,£}
	Слияние	(Uф,¬U ф)/ф	{U,ф},{¬U,ф}/{ф}
	Reductio	(U,¬U)/ |	{¬U},{U}/{}

Противоречие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.

Главное, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.

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

Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.

3.4 Поиск доказательства в системе резолюций

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

Пусть р представляет утверждение "Сократ — это человек", 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-программы, представленному в листинге 1. На рис. 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), и так до тех пор, пока не образуется пустая фраза.

Рис. 1. Дерево доказательства методом опровержения резолюций

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

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

Тема искусственного интеллекта всегда была в информатике "страной плохишей", населенной массой "неправильных" проблем, не поддающихся решению традиционными способами. Эта область привлекла внимание прежде всего разносторонних специалистов, которых не испугало ее открытое, лишенное всякой организации пространство, — людей, которых влечет задача узнать, как мы мыслим. Такие исследователи, как Марвин Минский (Marvin Minsky), Джон Мак-Карти (John McCarthy), Герберт Саймон (Herbert Simon), Пат Хейес (Pat Hayes), Дональд Мичи (Donald Michie) и Бернард Мельтцер (Bernard Meltzer), стали первопроходцами для тех, кто следовал за ними по пути, пролегающем через информатику, психологию и математическую логику.

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

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

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

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

Список литературы:

1. А.Н. Адаменко, А.М. Кучуков. Логическое программирование и Visual Prolog

СПб.: БХВ—Петербург, 2003.

2. Братко И. Алгоритмы искусственного интеллекта на языке PROLOG. М.: «Вильямс», 2004.

3. Джексон П. Введение в экспертные системы.-Москва, С. Петербург, Киев: Изд. дом "Вильямс", 2002

4. Дж. Доорс, А. Рейблейн, С. Вадера.Пролог - язык программирования будущего. М.: Финансы и статистика, 1990

5. Дюбуа Д., Прад А. Теория возможностей. Приложения к
представлению знаний. -М.: Радио и связь, 1995

6. Корнеев В.В., Гарев А.Ф., Васюшин СВ., Райх В.В. Базы данных.
Интеллектуальная обработка информации. - М.: Изд-во "Нолидж",
2000

7. Мендельсон Э. Введение в математическую логику. М., 1976

8. Нечаев В.В., Панченко В.М., Свиридов А.П. Исследование операций
и теория систем. Основы статистической динамики знаний. Учебное
пособие.-М.: МИРЭА, 2000

9. Новиков П. С. Элементы математической логики. М., 1959

10. Попов Э.В. Экспертные системы реального времени. В: Открытые
системы, N2 (10), 1995

11. Хоггер К. Введение в логическое программирование М.: Мир, 1988

12. Черч А. Введение в математическую логику, т. I. М. 1960