Метод резолюций. 
Символический искусственный интеллект: математические основы представления знаний

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

Формальные теории

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

Давид Гильберт (нем. David Hilbert), 1862—1943 — выдающийся немецкий математик-универсал, внес значительный вклад в развитие многих разделов математики и теоретической физики.

«Теория доказательства… дает нам возвышенное чувство убеждения в том, что, по крайней мере, для математического ума не поставлены никакие границы и что он сам в состоянии проследить законы собственного мышления…»

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

Формальная теория — это структура, имеющая следующие четыре необходимые составляющие:

• • множество А символов, образующих алфавит формальной теории,
• • множество. Рслов в алфавите Л, Fc Л*, которые называются формулами теории;
• • подмножество В формул, BcF, которые называются аксиомами формальной теории;
• • множество отношений R на множестве формул, R a Fⁿ⁺ⁱ, которые называются правилами вывода формальной теории.

Множество символов А может быть конечным или бесконечным (счетным). Обычно для образования символов используют конечное множество букв, к которым, если нужно, приписываются в качестве индексов натуральные числа.

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

Множества А и Fb совокупности определяют язык, или сигнатуру формальной теории, традиционно обозначаемую как? = (A, F).

Множество аксиом В может быть конечным или бесконечным (но счетным). Если множество аксиом бесконечно, то обычно оно задается с помощью конечного множества схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Самым распространенным правилом порождения конкретных аксиом из схемы аксиом является правило подстановки.

Приведем поясняющий пример. В учебнике Э. Мендельсона^[1][2] сказано (цитируем с небольшими сокращениями и в тех обозначениях, которые приняты в этой книге): «Каковы бы ни были формулы Л, В и С, следующие формулы суть аксиомы:

Это нужно понимать в следующем смысле. Пусть строчные латинские буквы, связкип и —а также круглые скобки (и) входят в алфавит рассматриваемой формальной теории, а прописные латинские буквы не входят. Тогда написанные выражения, помеченные именами (А1), (Л2) и (АЗ), строго говоря, не являются формулами формальной теории, а значит не могут быть и аксиомами. Это именно схемы аксиом. Вместо параметров А, В и С можно подставить любые формулы, причем вместо всех вхождений какого-либо параметра должна быть подставлена одна и та же формула, и полученное выражение, которое уже будет являться формулой данной формальной теории (заметим в скобках, что это исчисление высказываний), объявляется аксиомой. В частности, если в схему (А1) подставить формулу (Ь —> а) вместо параметра Л, и формулу а вместо параметра В, (это кратко обозначают следующим образом: [(6 -> а)/Л, а/В]), то получится формула ((b —> а) —" (а —" (Ь —" а))), которая является правильно построенной формулой и аксиомой исчисления высказываний. Если к той же схеме (А1) применить подстановку (а —" а)/А, а/В|, то получится формула ((а —> а) —" (я —"(я —" а)))_} которая также является аксиомой исчисления высказываний. Множество аксиом исчисления высказываний бесконечно, хотя и может быть задано всего тремя схемами аксиом.

Для прикладных теорий аксиомы нередко делятся на два вида:

• 1) логические аксиомы, прямо заимствованные из базовой формальной теории (повторим, в нашем случае — из исчисления предикатов первого порядка);
• 2) внелогические аксиомы (также говорят предметные или собственные аксиомы), отражающие прикладную специфику и содержание конкретной прикладной области.

Введем еще два понятия, относящиеся к формулам и аксиомам.

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

Если при этом время работы алгоритма распознавания ограничено полиномом от длины записи формулы, то говорят, что теория эффективно распознаваема.

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

Если при этом время работы алгоритма отнесения к аксиомам ограничено полиномом от длины записи формулы, то говорят, что теория эффективно аксиоматизируема.

Множество правил вывода R чаще всего конечно. Каждое правило вывода R е R является (п + 1)-местным отношением над множеством формул F, т. е. множеством кортежей вида (F_v …, F_rv F_w+1), где F_{ е F. Формулы Fj, …, F_n называют посылками, а формулу F"₊₁ —

заключение

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

• [1] Чаще всего это связано с шифрованными диалогами, когда предшествующий контекствлияет на правила построения последующих сообщений. Внешние обстоятельства могутвлиять на представление правил в системах продукций, интегрирующих несколько слабо-пересекающихся предметных областей со специфичными диалектами, когда, скажем, формула «/++» может трактоваться как правильное или неправильное арифметическое выражение в зависимости от перехода в контекст языка Си.
• [2] Мендельсон 3.

  Введение

  в математическую логику.