Логическое программирование
Формальные языки
Еще в конце 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 году.