н. ф. в виде «свертки Д. Н. Ф.» [22, 23];

В третьих, выразительные возможности этих метаисчислений должны быть достаточны для формализации различных методов и тактик поиска вывода. В этом смысле подход, заложенный при создании языка ПРОЛОГ, предполагающий жесткое замыкание на единственный метод резолюций, представляется не совсем удовлетворительным. Более перспективным представляется создание скорее «заготовки» исчисления, в которую можно внедрять самые различные методы. Достаточно последовательно эта идея проведена при построении системы «DEDUCTIO» [26]. Основой для реализации этой идеи в рамках проекта при написании машинной программы (см. ниже) послужили работы [19, 20].

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

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

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

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

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

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

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

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

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

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

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

Рассмотрим работу машинной реализации программы на базе исчисления чисел с индексами для проверки общезначимости пропозициональных формул. Функционально она состоит из следующих блоков:

n блок перевода пропозициональных формул в Д.