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

Трудности, возникшие при реализации программы, могут быть разделены на две группы. Во-первых, первоначальный вариант ОМ был достаточно жестко привязан к работе с д. н. ф., поэтому необходимо было либо «расширить» область действия ОМ на работу с другими формулами, либо предложить достаточно быстрый алгоритм перевода любой формулы (особенно к. н. ф.) в дизъюнктивную нормальную форму. Эта проблема была решена по второму варианту созданием такого алгоритма [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.
С.Л. Катречко

От логический исчислений к интеллектуальным системам (на базе обратного метода С.Ю. Маслова)

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

Для характеристики классических логических исчислений, построенных к середине 30-ых годов ХХ века (среди них можно выделить три основных типа систем: аксиоматические (гильбертовские) исчисления, секвенциальные (генценовские) исчисления и системы натурального вывода), были выделены три главных критерия. Прежде всего, любое логическое исчисление должно быть непротиворечивым. Во-вторых, оно, по возможности, должно обладать свойством полноты. В-третьих, желательно, чтобы исчисление было разрешимым. По этим критериям, самым «благополучным» логическим исчислением являлось, бедное в выразительном отношении, пропозициональное исчисление, обладающее всеми тремя свойствами. Более богатое в выразительном отношении исчисление предикатов, являясь непротиворечивым и полным, уже не обладает свойством разрешимости (теорема Черча — Россера). А еще более богатые в выразительном отношении системы первопорядковой арифметики не обладают свойством полноты (теорема Геделя).