Иллюстрированный самоучитель по введению в экспертные системы

Логическое программирование

• Формальные языки

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

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

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

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

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

• Язык PROLOG

  Фразы Хорна (Horn clause) представляют собой подмножество фраз, содержащих только один позитивный литерал. В общем виде фраза Хорна представляется выражением. | В языке PROLOG эта же фраза записывается в таком виде (обратите внимание на символ точки в конце): р: -q1,…,qn.

• Опровержение резолюций. Принцип резолюций.

  В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation).

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

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

• Процедурная дедукция в системе PLANNER

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

• PROLOG и MBASE. Правила поиска в языке PROLOG.

  Ранее мы уже видели, что фразу, содержащую предположение, можно представить с помощью исчисления предикатов первого порядка. Фраза: | "Если философ выиграет у кого-нибудь в забеге, то этот человек будет им восхищен" в формализме предикатов приобретет вид формулы: (любой A) (любой Y)(PHILOSOPHER(X)^BEATS(X, Y) ADMJRE(Y, X)).

• Управление поиском в системе MBASE

  Один из распространенных способов управления поиском в применении к доказательству какого-либо утверждения – тщательное упорядочение базы данных. При поиске нужных фактов или правил исполнительная система языка PROLOG просматривает базу данных от начала до конца.

• Рекомендуемая литература. Упражнения.

  Четкое изложение основных концепций теории доказательств в математической логике читатель найдет в работе Эндрюса [Andrews, 1986]. | Я также рекомендую познакомиться с книгой [Quine, 1979] – переизданием классического труда, опубликованного впервые еще в 1940 году.