С.Л. Катречко

Интеллектуальные системы на базе обратного метода С.Ю. Маслова <**>

К методологии построения интеллектуальных систем

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

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

3.   Наиболее перспективной методологией в этом направлении является переход к мета-исчислениям, в которых за счет дополнительной информации о структуре формуле (структурной информации) удается поиск вывода организовать более эффективно. Для этого создаваемые метаисчисления должны не только «наследовать» свойства исходных исчислений, но и учитывать особенности выводимых формул, т.е. должны быть формульно-ориентированными. Выразительные возможности этих мета-исчислений должны быть достаточны для формализации различных методов и тактик поиска вывода (в этом смысле подход: представленный в языке ПРОЛОГ, жестко замкнутый на единственный метод резолюций, представляется не совсем удовлетворительным).

4.   Существенный прогресс в организации поиска вывода связан с переходом к от языка к метаязыку, в котором возможно представление новых абстракций и, на их основе, новых допустимых правил вывода, существенно сокращающих время поиска. Эффективность такого перехода к новому метаязыку доказывает история математики, когда за счет перехода к «языку метапеременных Х и У» удалось найти общий метод решения квадратных уравнений. Достаточно нагляден в этом отношении и следующий (более логический) пример. Пусть нам дано аксиоматическое исчисление:

          аксиома 1: A=A                                                              A  [B],   B = С

          аксиома 2: (A=B)=(B= А)                правило вывода:   -------------------  , 

          аксиома 3: (A=(B=C) = ((A = B)= С)                                    А  [С]                     

     в котором необходимо построить вывод формулы W:

                                (P= Q) = ((Q = R) = (R = P))             

Вывод формулы W в данном исчислении занимает около двух страниц. Однако Р. Вейхрауху удалось значительно упростить данную задачу, предложив следующее правило (метаправило) для исчислений подобного типа: Каждое высказывание W, построенное только из пропозициональных переменных с помощью связки эквивалентности "=" таким образом, что любая пропозициональная переменная p входит в W четное число раз (подчеркнуто мной — К.С.), является теоремой [1].

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

5.   Тем самым, можно сформулировать две базовые идеи теории поиска вывода:

v   Введение новых объектов (путем использования метапеременных), которые замещают фиксированные значения переменных «нижнего» уровня.

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

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

Построение интеллектуальных систем на базе обратного метода

В качестве базы для построения логико-эвристических систем  был выбран обратный метод С. Ю. Маслова (ОМ) [2]. Это объясняется двумя причинами. Во-первых, ОМ представляет собой метаязык, предназначенный для выражения дополнительной структурной информации, релевантной для более эффективного поиска вывода:

§      информации о «зацепленности» литер (контрарных пар) формулы для пропозиционального случая;

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

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

Программа ОМ для пропозиционального исчисления.

Трудности, возникшие при реализации программы, могут быть разделены на две группы. Во-первых, первоначальный вариант ОМ был достаточно жестко привязан к работе с д. н. ф., поэтому необходимо было либо «расширить» область действия ОМ на работу с другими формулами, либо предложить достаточно быстрый алгоритм перевода любой формулы (особенно к. н. ф.) в дизъюнктивную нормальную форму. Эта проблема была решена по второму варианту созданием такого алгоритма [4]. Более принципиальные трудности связаны с характером работы ОМ, который, породив некоторое число исходных благоприятных наборов (составленных из всех наборов контрарных пар литер),начинает получать новые благоприятные наборы путем «склеивания» уже имеющихся благоприятных наборов, с целью получения «пустого» (ноль-членного) благоприятного набора. Поскольку, в общем случае, эта процедура выполняется чисто механически, перебором всех возможных «склеек», то эффективность ОМ связана с уменьшением числа благоприятных наборов на каждом этапе порождения благоприятных наборов. Для решения этой задачи было предложено следующее:

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

q      Для уменьшения порождения новых благоприятных наборов было использованы различные более специальные тактики получения «пустого» набора. Например, при получении какого-либо однолитерного благоприятного набора дальнейший поиск может сводиться к нахождению однолитерного набора(ов), составленного(ых) из другой(их) литер данного дизъюнкта, «склеиванием» которых и может быть решена задача получения «пустого» благоприятного набора. Однако одним из самых мощных ограничителей порождения множества излишних в процессе поиска вывода наборов выступала следующая лемма: если получен некоторый благоприятный поднабор, то в использовании всех его наднаборов в выводе нет необходимости: ибо при этом мы получим не более чем наднаборы уже возможных (полученных или могущих быть полученными) благоприятных наборов.

Целесообразно также, при работе с ОМ учитывать идеологию систем натуральных выводов, связанных с введением допущений, поскольку за счет этого возможно существенное сокращение используемых наборов [5].

==============

<**> — тезисы доклада на 1-ом Всероссийском философском конгрессе (секция «Логика и философская логика»). Санкт-Петербург, июнь 1997.

Литература:

1.     Weyhrauch R.W. Prolegomena to a theory of mechanized formal reasoning  //Artificial Intelligence, 1980, Vol. 13. P.133 - 170.

2.     Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, 1968, Т.98. С.26 - 87.

3.     Катречко С.Л. Обратный метод С. Ю. Маслова //Логика  и компьютер 2. — М., Наука, 1995, С. 62 - 75

4.     Царьков Д.В., Катречко С.Л. Об одном алгоритме приведение пропозициональных формул к д. н. ф. //Международная конференция (1-ые) «Смирновские чтения». — М., 1997.

5.     Катречко С.Л. Моделирование правила расщепления в обратном методе С. Ю. Маслова //Логические методы в компьютерных науках. — М., Институт Философии РАН, 1992, С. 125 - 141.