С.Л. Катречко
От
логический исчислений к интеллектуальным системам (на базе обратного метода
С.Ю. Маслова) <**>
Методологические
принципы построения интеллектуальных систем
Для характеристики классических логических исчислений,
построенных к середине 30-ых годов ХХ века (среди них можно выделить три
основных типа систем: аксиоматические (гильбертовские) исчисления,
секвенциальные (генценовские) исчисления и системы натурального вывода), были
выделены три главных критерия. Прежде всего, любое логическое исчисление должно
быть непротиворечивым.
Во-вторых, оно, по возможности, должно обладать свойством полноты. В-третьих,
желательно, чтобы исчисление было разрешимым. По этим критериям, самым
«благополучным» логическим исчислением являлось, бедное в выразительном
отношении, пропозициональное исчисление, обладающее всеми тремя свойствами.
Более богатое в выразительном отношении исчисление предикатов, являясь
непротиворечивым и полным, уже не обладает свойством разрешимости (теорема Черча — Россера). А еще более
богатые в выразительном отношении системы первопорядковой арифметики не
обладают свойством полноты (теорема
Геделя).
Уточняя вышесказанное, можно сказать, что главным критерием
логических исчислений в то время было свойство непротиворечивости, поскольку
основным назначением этих систем было обеспечение логической корректности, т.е. невозможности получения
с их помощью из истинных посылок ложных заключений. В этом смысле,
поскольку логические исчисления изначально не были предназначены для
организации эффективного (быстрого) поиска вывода, для их функционирования было
достаточно предложить любую логически корректную процедуру построения вывода,
которая могла быть процедурой полного перебора, например, алгоритмом
Британского музея. Более того, такая процедура гарантировала «полноту»
построения вывода: если вывод в принципе существует, то он с помощью процедуры
полного перебора будет найден.
Начиная с середины ХХ века, в связи с бурным развитием вычислительной
техники, наряду с тремя вышеперечисленными критериями логических исчислений
необходимо ввести еще один параметр оценки вычислительных систем — критерий эффективности.
В отличие от критерия разрешимости, который устанавливает принципиальную
(теоретическую) разрешимость логических исчислений, данный критерий является критерием практической
эффективности вычислительной системы и призван оценить эффективность (быстроту)
вычислительного алгоритма. Тем самым, суть новой проблемы, связанной с
развитием вычислительных систем, можно сформулировать в виде задачи перехода
от «медленных» процедур полного
перебора, имеющих экспоненциальную сложность, к более «быстрым» (эффективным)
алгоритмам, идеалом которых являются полиноминальные вычислительные алгоритмы.
При этом заметим, что, во-первых, критерий практической эффективности системы в
общем случае вступает в конфликт с «полнотой» поисковой процедуры, т.е. с
заведомым нахождением всех возможных решений, поскольку эффективность поисковой
процедуры предполагает отказ от процедур полного перебора. В этом смысле такие
процедуры являются «неполными» или «эвристиками», не гарантирующими в общем
случае нахождения решения (или всех существующих решений). В своей более
радикальной формулировке критерий эффективности предполагает отказ даже от логической
корректности, т.е. с целью повышения эффективности поисковых процедур возможно
построение «быстрых» сверхполных
алгоритмов, генерирующих решения, возможно выходящие за рамки логически
корректных.
Осмысление этой проблематики привело к возникновению новых теоретических дисциплин. Среди них
можно выделить следующие. Во-первых, в рамках вычислительной математики
появляется так называемая теория
сложности, одним из основных результатов которой было выявление знаменитой P = NP — проблемы и
возможных путей ее решения [1]. Несколько огрубляя суть дела, можно сказать, в
рамках этой дисциплины исследуется в основном «количественный» (сложностной)
аспект проблемы создания эффективных поисковых процедур.
Во-вторых,
возможно осмысление проблематики эффективности логических исчислений на более
«качественном» уровне, что привело к возникновению в рамках логики нового
раздела — теории поиска вывода (ТПВ).
К классическим исследованиям этого направления можно отнести работы
Д. Пойа [2], Хао Вана [3], С. Кангера [4], С.Ю. Маслова [5],
О.Ф. Серебрянникова [6], В.А. Смирнова [7]. Это достаточно молодая
область логики, которая, в отличие от логики, не ставит своей задачей (на
основе выявления логической формы) исследование правильных способов
рассуждений, а акцентирует свое внимание на вопросе «как строить (искать)
вывод?». Более точно рамки этого подхода можно определить так. С одной стороны,
предпринимается анализ существующих логических исчислений с целью исследования
их «эвристического» потенциала и возможностей построения на их базе логических»
систем с более эффективными поисковыми
процедурами. Т.е. для повышения эффективности поисковых процедур «логическая»
составляющая указанных систем должна быть дополнена некоторой «эвристической»
составляющей, призванной преодолеть полный перебор при построении вывода. С
другой стороны, при построении таких систем хотелось бы не выходить за рамки логически
корректными процедур, т.е. наложить на эвристические поисковые процедуры
требование не порождать при истинности посылок ложных заключений. Первоначально
определенные надежды возлагались на секвенциальные исчисления, в рамках которых
возможен «аналитический» подход к построению вывода «снизу вверх»; позже
внимание исследователей привлекли системы натурального вывода. Однако вскоре
стало ясно, что необходимо переходить к построению нового типа логических
исчислений — логико-эвристическим
или ин-теллектуальным системам [8].
Помимо этого основного требования к построению
«логико-эвристических» систем (требование их логической корректности), выделим
еще три существенные идеи, реализованные в рамках проекта.
Отметим, во-первых, что логико-эвристические
системы должны иметь характер метаисчислений,
т.е. надстраиваться над существующими логическими исчислениями. Выразительные
возможности языка построенных
метаисчислений должны сделать возможным представление новых абстракций и, на их
основе, новых допустимых правил вывода, существенно сокращающих время поиска.
Одним из аргументов в пользу эффективности такого перехода к новому метаязыку
может служить следующий факт из истории математики, когда за счет перехода к
«языку метапеременных) Х и У» удалось найти общий метод решения квадратных уравнений.
Обобщая этот подход можно сформулировать следующее методологическое правило,
активным приверженцем и пропагандистом которого был крупный российский философ
и логик В.А. Смирнов: переформулировка задачи на новом языке
(метаязыке) позволяет существенно упростить процедуру ее решения, а часто
просто превращает сложную задачу в тривиально решаемую. Достаточно нагляден
в этом отношении и следующий пример, приводимый в [8]. Пусть нам дано
аксиоматическое исчисление:
аксиома 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 четное число раз (выделено мной —
К.С.), является теоремой [9].
Данное правило позволяет "свести" доказательство некоторой формулы W к простому подсчету "четности" разных переменных, что значительно сокращает "вывод" данной формулы W. Это стало возможным за счет использования при построении вывода новой абстракции — понятия "четное число", и введения на его основе нового допустимого правила вывода, что в языке логики высказываний сделать невозможно.
В рамках реализации этой идеи было сделано следующее:
·
переход к логическим
исчислениям, использующим тернарные логические связки. В рамках проекта этот
подход реализован построением исчисления поиска на базе тернарной связки
«условной дизъюнкции» [10]. Отметим, что идея использования этой связки при
построении логических исчислений восходит к А. Черчу [11], а впервые была
реализована в работе российского логика Е. Сидоренко [12]);
·
переход к логическим
исчислениям с «временными» переменными (мета-переменными). В рамках проекта
этот подход реализован в работе [13]. Отметим, что в данном случае
сформулированное выше методологическое правило конкретизируется так: введение
новых объектов (путем использования «временных» метапеременных), которые
замещают фиксированные значения переменных «нижнего» уровня (авторство
этой идеи принадлежит С. Кангеру [4], Д. Правицу и Н. Шанину [5,
стр.100]);
Во-вторых, при построении «логико
— эвристических» исчислений целесообразно превратить их в
формульно-ориентированные метаисчисления, т.е. использовать идею «глобальной
обработки информации», предложенную в рамках ленинградской школы
математической логики (пионерские реализации этой идеи представлены в работах
[14, 15]). Суть этого подхода заключается в том, чтобы при построении вывода
формулы использовать дополнительную информацию о структуре формулы (структурной
информации) удается поиск вывода организовать более эффективно. Для этого
создаваемые метаисчисления должны не только «наследовать» свойства исходных
исчислений, но и учитывать особенности выводимых формул, т.е. быть
формульно-ориентированными. В этом смысле исчисления поиска вывода можно
трактовать как метаисчисления Иb,f, построенного по исходному исчислению b и формуле f. Выводимость в построенном метаисчислении особого объекта эквивалентна выводимости f в исходном исчислении b.
К этому классу исчислений можно отнести исчисления обратного метода [16],
исчисления метода резолюций [17] и расщеплений [18], а также построенные С. Катречко
исчисления чисел с индексами [19, 20, 21]. В рамках реализации этой идеи было
сделано следующее:
·
построение машинной
реализации исчислений чисел с индексами для пропозициональной логики (см.
распечатку текста программы, написанной на языке СИ++ в приложении 1), в рамках
которой предложен оригинальный алгоритм преобразования формул в
д. н. ф. [22, 23];
·
в общих чертах
сформулированы принципы написания программы автоматического доказательства
теорем на базе предложенного исчисления чисел с индексами для исчисления предикатов
[20, 23, 24];
·
сформулирована
оригинальная идея о возможности повышения эффективности исчислений поиска за
счет перехода к новой структуре представления формул и выводов. Первоначально
эта идея была высказана [25], как идея возможности структурной специализации
выводов в секвенциальных системах и системах натурального вывода. Чуть позже
она была использована при построении исчислений с «условной дизъюнкцией». В
рамках данного проекта она получила дальнейшее развитие при формулировании
оригинального алгоритма перевода формулы в дизъюнктивной нормальной форме в
качестве использования более компактного представления д. н. ф. в
виде «свертки Д. Н. Ф.» [22, 23];
В третьих, выразительные возможности этих метаисчислений
должны быть достаточны для формализации различных методов и тактик поиска
вывода. В этом смысле подход, заложенный при создании языка ПРОЛОГ, предполагающий жесткое
замыкание на единственный метод резолюций, представляется не совсем
удовлетворительным. Более перспективным представляется создание скорее
«заготовки» исчисления, в которую можно внедрять самые различные методы.
Достаточно последовательно эта идея проведена при построении системы «DEDUCTIO» [26]. Основой для
реализации этой идеи в рамках проекта при написании машинной программы (см.
ниже) послужили работы [19, 20].
Построение
интеллектуальных систем на базе обратного метода
В качестве базы для построения логико-эвристических систем был выбран обратный метод
С.Ю. Маслова (ОМ) [16]. Это объясняется двумя причинами. Во-первых, ОМ
представляет собой метаязык, предназначенный для выражения дополнительной структурной
информации, релевантной для
более эффективного поиска вывода:
o информации о «зацепленности» литер (контрарных пар) формулы
для пропозиционального случая;
o информации об возможных ограничениях на необходимые подстановки
переменных в предикатные формулы.
Во-вторых, ОМ является достаточно
мощным самостоятельным методом поиска, сопоставимым с другими методами поиска,
который может быть сделан более эффективным как за счет «внутренних» резервов
(разработка различных тактик его
применения), так и за счет «внешнего» подключения к ОМ других мощных методов
поиска (речь идет, прежде всего, от методах резолюций и расщепления [17, 18]).
Программа для пропозиционального исчисления
Трудности, возникшие при реализации программы, могут быть разделены
на две группы. Во-первых, первоначальный вариант ОМ был достаточно жестко привязан
к работе с д. н. ф., поэтому необходимо было либо «расширить» область
действия ОМ на работу с другими формулами, либо предложить достаточно быстрый
алгоритм перевода любой формулы (особенно к. н. ф.) в дизъюнктивную
нормальную форму. Эта проблема была решена по второму варианту созданием такого
алгоритма [22, 23]. Более
принципиальные трудности связаны с характером работы ОМ, который, породив
некоторое число исходных благоприятных наборов (составленных из всех наборов
контрарных пар литер), начинает получать новые благоприятные наборы путем
«склеивания» уже имеющихся благоприятных наборов, с целью получения «пустого»
(нольчленного) благоприятного набора. Поскольку, в общем случае, эта процедура
выполняется чисто механически, перебором всех возможных «склеек», то
эффективность ОМ связана с уменьшением числа благоприятных наборов на каждом
этапе порождения благоприятных наборов. Для решения этой задачи было предложено
следующее:
n
Для уменьшения числа
исходных благоприятных наборов целесообразно произвести «прополку» исходной
д. н. ф. с целью исключения из нее «нерелевантной» для поиска вывода
информации. Для этого из д. н. ф. исключаются повторяющиеся
д. н. ф., оставляются самые короткие из имеющихся д. н. ф.
(т.е. самые «сильные» д. н. ф.), а также происходит «прореживание»
д. н. ф. путем исключения из состава д. н. ф. однолитерных
дизъюнктов с одновременным вычеркиванием из остающихся дизъюнктов контрарных
литер. Тем самым, исходная д. н. ф. и, следовательно, число исходных
благоприятных наборов уменьшается.
n
Для уменьшения
порождения новых благоприятных наборов было использованы различные более специальные
тактики получения «пустого» набора. Например, при получении какого-либо
однолитерного благоприятного набора дальнейший поиск может сводиться к
нахождению однолитерного набора(ов), составленного(ых) из другой(их) литер
данного дизъюнкта, «склеиванием» которых и может быть решена задача получения
«пустого» благоприятного набора. Однако одним из самых мощных ограничителей
порождения множества излишних в процессе поиска вывода наборов выступала
следующая лемма: если получен некоторый благоприятный поднабор, то в использовании всех
его наднаборов в выводе нет необходимости: ибо при этом мы получим не более чем
наднаборы уже возможных (полученных или могущих быть полученными) благоприятных
наборов.
Целесообразно также, при работе с ОМ учитывать идеологию
систем натуральных выводов, связанных с введением допущений, поскольку за счет
этого возможно существенное сокращение используемых наборов [20].
В рамках реализации проекта Д.В. Царьковым была
написана программа, реализующая обратный метод С.Ю. Маслова для
пропозициональной логики. Аналогичная программа для логики первого порядка
находится в стадии отладки.
Рассмотрим работу
машинной реализации программы на базе исчисления чисел с индексами для проверки
общезначимости пропозициональных формул. Функционально она состоит из следующих
блоков:
n
блок перевода
пропозициональных формул в Д. Н. Ф. (далее ДНФ);
n
блок упрощения ДНФ;
n
блок работы
собственно обратного метода.
Продемонстрируем работу каждого блока подробнее.
Обратный метод С.Ю. Маслова
работает с формулой, представленной в виде дизъюнктивной нормальной формы
(ДНФ), поэтому необходимо преобразование введенной формулы. Блок перевода в ДНФ
строит по древесному представлению формулы ее ДНФ по оригинальному алгоритму,
более подробно изложенному в [19, 20]. Главное отличие данного метода от других
алгоритмов в том, что он не строит полноценную ДНФ, а строит свернутую форму
ДНФ — свертку ДНФ. Результат работы этого алгоритма (первого блока программы)
можно продемонстрировать на простом примере (пример
1).
Пусть нам дана следующая формула (aÚb) & (~aÚbÚ~c). Здесь знак ~ обозначает отрицание, & — конъюнкцию, Ú — дизъюнкцию. При применении стандартного алгоритма,
использующего правила де Моргана получим следующую ДНФ D1: (a&~a) Ú (a&b) Ú (a&~c) Ú (b&~a) Ú (b&b) Ú (b&~c).
При применении нашего
оригинального алгоритма мы получим следующую свертку ДНФ:
~c (с 1 (с шагом 3) до 6)
b (с 2 (с шагом 3) до 6)
~a (с 3 (с шагом 3) до 6)
b (с 1 до 3)
a (с 4 до 6)
Первая запись свертки
ДНФ означает следующее. Литера ~c
(литера с отрицанием) встречается в
первом дизъюнкте, и далее она встречается в каждом последующем третьем
дизъюнкте (в каждом последующем дизъюнкте с шагом 3) до дизъюнкта не
превышающего номера 6 (можно отметить, что представленная выше свертка ДНФ показывает,
что число дизъюнктов данной ДНФ не более 6), т.е. литера ~c встречается в дизъюнктах 1 и 4, а следующий третий дизъюнкт
имеет номер 4+3=7, который больше 6, что свидетельствует о том, что литера ~c не встречается более в данной ДНФ
(соответственно вторая (третья) строка свертки означает, что литера b (~a) встречается во втором (третьем) дизъюнкте, и далее она встречается в каждом последующем третьем
дизъюнкте, т.е. в дизъюнкте 5 (6). Четвертая (пятая) запись свертки a(4
до 6) [b (с 1 до 3)] означает,
что литера a [b]
встречается в дизъюнктах с 4 по 6 [c 1 по 3]
включительно. Тем самым, представленную выше свертку ДНФ можно развернуть в
полноценную ДНФ следующего вида: (b&~c) Ú (b&b) Ú (b&~a) Ú (a&~c) Ú (a&b) Ú (a&~a), что с точностью до перестановки дизъюнктов совпадает с D1, построенной
с помощью стандартного преобразования формул в ДНФ .
Для
наглядности описания двух последующих блоков программы (блока упрощения ДНФ и
блока работы собственно обратного метода) рассмотрим еще один пример (пример
2), с помощью которого попробуем рассказать о наиболее существенных
моментах работы алгоритма.
Блок упрощения
опирается на [20] и производит следующие действия:
1.
Если в ДНФ имеются
однолитерные дизъюнкты (ОД) p и ~p, то ДНФ общезначима;
2.
Если некоторая
переменная входит в ДНФ с одним знаком, то удаляем все дизъюнкты, содержащие
эту переменную;
3.
Если в ДНФ имеется
какой-то однолитерный дизъюнкт p то
выполняем следующие действия:
·
удаляем все дизъюнкты
вида p & … (правило поглощения);
·
все дизъюнкты вида ~p & s & … заменяем на
дизъюнкты вида s & …, а после
этого удаляем сам однолитерный дизъюнкт p
(правило
удаления однолитерных дизъюнктов).
(~a&d) Ú (b&a) Ú (~a&~d ) Ú (~b&~d) Ú (~b&d)
После этого начинает работу блок обратного метода. Прежде
чем описать его работу, изложим вкратце суть метода.
Обратный метод
оперирует с наборами. Набор имеет вид [i/k, j/l, …]
(m, n, …), где i, j,
… — номера дизъюнктов в ДНФ, а k, l — номера литер в i и j дизъюнктах соответственно. Числа m, n образуют зависимость набора и представляют
собой номера дизъюнктов. В программе есть база данных, в которой хранятся все
наборы. Эту базу в дальнейшем мы будем называть базой наборов.
Собственно обратный
метод состоит в следующем. Мы выбираем из базы наборов ряд наборов вида [i/1, …] (…), [i/2 ,…] (…), …, [i/n, …] (…), где n — длина i-го дизъюнкта. Затем мы строим новый
набор, в котором присутствуют все члены всех выделенных наборов, кроме членов
вида i/k, а зависимость представляет
собой объединение всех зависимостей плюс элемент i. Это и есть основное правило работы алгоритма — правило склейки, соответствующее
правилу Б обратного метода. При этом должен выполняться ряд требований на
наборы. Если в процессе многократного применения данного правила удается
вывести пустой набор (т.е. набор вида [ ] (…)), то исходная ДНФ общезначима.
Рассмотрим теперь
работу блока обратного метода. Сначала мы
формируем базу наборов для обратного метода. Для каждой переменной p
проделываются следующие действия. Пусть дизъюнкт i содержит переменную p на k-м месте, а дизъюнкт j
— ~p
на l-ом месте. Тогда в базу наборов добавляется набор [i/k, j/l] ( ) — замкнутый набор, или набор с пустой
зависимостью.
(~a&d) Ú (b&a) Ú (~a&~d ) Ú (~b&~d) Ú (~b&d)
#1 [2/1 4/1] ( ) — наборы, соответствующие переменной b
#2 [2/1 5/1] (
)
#3 [1/1 2/2] ( ) — наборы,
соответствующие переменной a
#4 [2/2 3/1] (
)
#5 [1/2 3/2] ( ) — наборы, соответствующие переменной d
#6 [1/2 5/2] ( )
#7 [3/2 4/2] ( )
#8 [4/2 5/2] (
)
Здесь #n
означает, что данный набор записан под номером n; все номера наборов уникальны.
После этого мы
начинаем искать наборы, для которых возможно применить правило склейки. На эти
наборы накладываются следующие ограничения:
·
Если в одном из
наборов в зависимости есть число s, то в других наборах не должно быть членов
вида s/r;
·
Если в каком-нибудь
наборе есть член вида s/r, то ни в одном из других наборов не должно быть
членов s/t;
·
Ни один из наборов не
должен иметь в зависимости число i;
Если все эти
требования выполнены, то создается новый набор по указанному выше правилу; он
добавляется в базу наборов. Так продолжается до тех пор, пока мы не получим
пустой набор или пока не будут построены все возможные наборы. В первом случае
исходная формула общезначима, во втором – нет.
Для упрощения
поиска в базе наборов в программе создается списочная таблица: для каждых i, j она предоставляет список наборов,
которые содержат член i/j. Для
рассматриваемого примера 2 таблица имеет следующий вид:
|
№ дизъ. |
Индекс |
№ набора |
|
1 |
1 |
3 |
|
1 |
2 |
5,6 |
|
2 |
1 |
1,2 |
|
2 |
2 |
3,4 |
|
3 |
1 |
4 |
|
3 |
2 |
5,7 |
|
4 |
1 |
1 |
|
4 |
2 |
7,8 |
|
5 |
1 |
2 |
|
5 |
2 |
6,8 |
При порождении
новых наборов, в результате работы правила склейки, таблица изменяется соответствующим
образом.
Для ускорения
работы программы необходимо на каждом шаге, по возможности, уменьшить число
наборов, могущих участвовать в выводе. Это связано с тем, что предложенный
алгоритм «механически» строит все возможные «склейки» существующих наборов (об
этом смотри выше). Для уменьшения числа участвующих в выводе наборов
предусмотрено несколько режимов работы алгоритма:
·
Наиболее существенный
выигрыш дает лемма о поднаборности [20]. Она говорит, что если мы получили набор,
являющийся наднабором некоторого
имеющегося набора, то вновь полученный набор можно исключить из дальнейшего
рассмотрения. Использование этой леммы позволяет сократить перебор. Например,
если в базе наборов имеется набор [3/1, 4/2] (...) (набор a), а построенный набор имеет вид [3/1, 4/2, 6/4] (...), то новый набор, являющийся наднабором набора
a, не дает ничего
нового: он «слабее» того «поднабора» a, который уже имеется
в базе наборов. Поэтому его можно не рассматривать в дальнейшем. Наоборот, если
построен набор [4/2] (…),
который является поднабором набора a, то он переносится в базу наборов, а набор [3/1, 4/2] (…)
(набор a), соответственно, удаляется из базы наборов.
·
Другой способ
сокращения числа наборов (и соответственно, времени поиска) основывается на
том, что правило склейки является «локальным» правилом, позволяющим за одно
свое применение удалить не более одного члена из состава исходных наборов.
Поэтому можно предложить следующую тактику работы алгоритма. Для получения
пустого набора нам необходимо иметь совокупность однолитерных наборов [i/1] (…), …, [i/n] (…) для некоторого i. Тогда вместо того, чтобы искать
пустой набор, зафиксируем число i и
будем последовательно искать наборы [i/1] (…)
,…, [i/n](…). При этом, пытаясь
вывести набор [i/1] (…), мы можем не
рассматривать наборы, содержащие члены i/2, … , i/n, что существенно сокращает число наборов, участвующих в
выводе на этом этапе. Если мы найдем все такие наборы, то ДНФ выводима; иначе
(если мы не смогли построить какой-нибудь из этих наборов) мы удаляем из базы
все наборы, содержащие элемент i/j, и повторяем
поиск. Эта тактика, первоначально предложенная в [20], является аналогом метода расщепления.
Теперь, по имеющейся базе наборов реализуем обратный метод для нашего примера. Мы рассмотрим вариант, когда он работает, используя тактику расщепления с расщеплением и лемму о поднаборности, поскольку это наиболее сложный случай работы алгоритма. Итак, мы имеем восемь исходных наборов:
#1 [2/1 4/1] ( )
#2 [2/1 5/1] ( )
#3 [1/1 2/2] ( )
#4 [2/2 3/1] ( )
#5 [1/2 3/2] ( )
#6 [1/2 5/2] ( )
#7 [3/2 4/2] ( )
#8 [4/2 5/2] (
)
Допустим, что наш алгоритм начал
свою работу с «расщепления» последнего дизъюнкта и алгоритм пытается построить
набор, содержащий в теле только элемент 5/2.
При этом набор 2 исключается из рассмотрения,
т.к. он содержит элемент 5/1 (см.
тактику расщепления). Программа последовательно порождает следующие наборы:
#9
[2/2 5/2] (1/0) из наборов 3, 6
#10
[2/2 3/2] (1/0) из наборов 3, 5
#11
[3/2 4/1] (1/0 2/0) из наборов 1, 10
#12
[4/1 5/2] (1/0 2/0) из наборов 1, 9
#13
[3/1 4/1] (2/0) из наборов 1, 4
#14
[1/1 4/1] (2/0) из наборов 1, 3
#15
[4/1] (1/0 2/0 3/0) из наборов 13, 11
---
Набор 14 was
skipped
by 15
--- Набор 13 was skipped by 15
--- Набор 12 was skipped by 15
--- Набор 11 was skipped by 15
--- Набор 1 was skipped by 15
После построенного
набора указывается, из каких наборов он был построен.
Получив набор 15, имеющий размер 1, мы можем, на основании леммы о поднаборности, исключить из базы наборов исходный набор 1 и полученные в результате работы алгоритма наборы 11, 12, 13, 14. Тем самым наша база принимает следующий вид:
#2 [2/1 5/1] ( )
#3 [1/1 2/2] ( )
#4 [2/2 3/1] ( )
#5 [1/2 3/2] ( )
#6 [1/2 5/2] ( )
#7 [3/2 4/2] ( )
#8 [4/2 5/2] ( )
#9
[2/2 5/2] (1/0)
#10
[2/2 3/2] (1/0)
#15 [4/1] (1/0 2/0 3/0)
«Прополов»
базу наборов, продолжим работу алгоритма:
#17 [2/2] (1/0 3/0) из наборов 4,
10
--- Набор 10 was
skipped
by 17
--- Набор 9 was skipped by 17
--- Набор 4 was skipped by 17
--- Набор 3 was skipped by 17
Получив
набор 17, мы можем снова, на
основании леммы о поднаборности, провести «прополку» базы наборов и исключить
из нее исходные наборы 3,4 и полученные
в результате работы алгоритма наборы 9,
10.
#20 [5/2] (1/0 2/0 3/0 4/0) из
наборов 15, 8
---
Набор 8 was
skipped
by 20
--- Набор 6 was skipped by 20
Получив набор 20
исключаем из базы наборов исходные наборы 6,
8.
Итак, получен искомый набор — набор 20. Он имеет тело, состоящее только из элемента 5/2. В этот момент в базе присутствуют наборы:
#2 [ 2/1
5/1 ] ( )
#5 [ 1/2 3/2 ]
( )
#7 [ 3/2
4/2 ] ( )
#15
[ 4/1 ] ( 1/0 2/0 3/0 )
#17
[ 2/2 ] ( 1/0 3/0 )
#20 [ 5/2 ] ( 1/0 2/0 3/0 4/0 ) из наборов 15, 8
Теперь приступим к поиску набора [5/1] (...), поскольку получив этот набор мы можем «склеивая» его с уже
полученным набором 20, получить
пустой набор. Отметим, что в рамках тактики расщепления, при построении набора [5/1] (...) мы исключаем из
нашего рассмотрения набор 20,
т.к. он содержит элемент 5/2. Набор [5/1] (...) может быть построен за один шаг из наборов 2, 17:
#22
[ 5/1 ] ( 1/0 2/0 3/0 ) из наборов 2, 17
--- Набор 2 was skipped by 22 (исключаем из базы исходный набор 2).
Итак, набор [5/1] построен. Это
означает, что формула общезначима. Далее алгоритм печатает дерево наборов, приведшее
к успеху, по которому может быть восстановлено секвенциальное дерево:
#22
[5/1] (1/0 2/0 3/0) из наборов
2, 17
#2
[2/1 5/1] ( )
#17
[2/2] (1/0 3/0) из наборов 4, 10
#4
[2/2 3/1] ( )
#10
[2/2 3/2] (1/0) из наборов 3, 5
#3
[1/1 2/2] ( )
#5
[1/2 3/2] ( )
#20
[5/2] (1/0 2/0 3/0 4/0) из наборов 15, 8
#15
[4/1] (1/0 2/0 3/0) из наборов 13, 11
#13
[3/1 4/1] (2/0) из наборов 1, 4
#1
[2/1 4/1] ( )
#4
[2/2 3/1] ( )
#11
[3/2 4/1] (1/0 2/0) из наборов
1, 10
#1
[2/1 4/1] ( )
#10
[2/2 3/2 ] (1/0) из наборов 3, 5
#3
[1/1 2/2] ( )
#5
[1/2 3/2] ( )
#8
[4/2 5/2] ( )
#17
[2/2] (1/0 3/0) из наборов 4, 10
#4
[2/2 3/1] ( )
#10
[2/2 3/2] (1/0) из наборов 3, 5
#3
[1/1 2/2] ( )
#5
[1/2 3/2] ( )
#15
[4/1] (1/0 2/0 3/0) из наборов 13, 11
#13
[3/1 4/1] (2/0) из наборов 1, 4
#1
[2/1 4/1] ( )
#4
[2/2 3/1] ( )
#11
[3/2 4/1] (1/0 2/0) из наборов 1, 10
#1
[2/1 4/1] ( )
#10 [2/2 3/2] (1/0) из наборов 3, 5
В заключении
сформулируем еще одну тактику ограничения числа участвующих в выводе наборов.
Она состоит в следующем. Пусть набор, помимо элементов и зависимости,
характеризуется еще одним числом – поколением. Все замкнутые наборы являются наборами нулевого поколения, все
наборы, построенные из них – наборы первого поколения, и т.д. Сначала мы строим
наборы первого поколения – при этом нет никаких сложностей. Когда все такие
наборы построены, переходим к наборам второго поколения. При этом надо
придерживаться следующих ограничений:
·
Хотя бы один из
отобранных наборов должен быть из первого поколения;
·
Ни один из наборов не
может быть из второго поколения.
После того, как все
наборы второго поколения построены, переходим к наборам третьего поколения. Так
продолжается до тех пор, пока мы не построим пустой набор (тогда ДНФ
общезначима). Если на каком-то этапе мы не можем построить ни один новый набор,
то можно сделать вывод о необщезначимости ДНФ.
В нашем случае
наборы 1 — 8 будут наборами 0-го
поколения, наборы 9, 10, 13, 14 —
наборами первого поколения. Набор 11
будет набором второго поколения и будет построен только после 14-го. Можно заметить, что применение этой тактики в нашем случае
неэффективно: тактика при небольших формулах (глубина вывода которых не
превышает 3 шага) несколько тормозит работу программы, но дает существенный
выигрыш при больших формулах.
============
<**> — данный текст (в соавторстве с Царьков Д.В.) подготовлен в качестве итогового научного отчета по гранту РГНФ № 096-03-04143 (исследовательский проект "От логических исчислений к интеллектуальным системам").
1.
Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. — М.: Мир, 1982.
2.
Пойа Д. Как решать задачу. — М.: Учпедгиз, 1959.
3.
Ван Хао На пути к механической математике //Кибернетический
сборник, 1962 № 5. С. 114 - 165.
4.
Кангер С. Упрощенный метод доказательства для элементарной
логики //Математическая теория логического вывода. — М.: Наука, 1967.
С. 200 - 208.
5.
Маслов С.Ю. Теория дедуктивных систем и ее применения. — М.:
Радио и связь, 1986.
6. Серебрянников О.Ф. Эвристические принципы и логические исчисления. — М.:
Наука, 1970.
7.
Смирнов В.А. Формальный вывод и логические исчисления. — М.:
Наука, 1972.
8.
Катречко С.Л. Бесконечность и теория поиска вывода
//Бесконечность в математике: философские и исторические аспекты. — М.,
«Янус-К», 1997.
9. Weyhrauch R.W. Prolegomena to a theory of mechanized
formal reasoning //Artificial Intelligence, 1980, Vol. 13. P. 133 - 170.
10. Катречко
С.Л. Исчисление поиска вывода с «условной дизъюнкцией» //XI Международная
конференция "Логика, методология, философия науки», Т.2. Москва — Обнинск,
1995.
11. Черч А.
Введение в математическую логику. — М.: ИЛ., 1960
12.
Сидоренко Е.А. Пропозициональное
исчисление с условной дизъюнкцией //Методы логического анализа. — М.:
Наука,1977. С. 150 - 159.
13. Катречко
С.Л. От логики к теории поиска вывода
//Международная конференция «Развитие
логики в России: итоги и перспективы», М., 1997.
14. Алгорифм
машинного поиска естественного логического вывода в исчислении высказываний //Н.А. Шанин, Г.В. Давыдов,
С.Ю. Маслов и др. — М. — Л., Наука, 1965.
15. Давыдов
Г.В. Некоторые замечания о поиске вывода в
исчислении предикатов //Записки научных семинаров ЛОМИ АН СССР, 1968.
Т.8. С.8 - 20.
16. Маслов
С.Ю. Обратный метод установления выводимости для логических исчислений //Труды
математического института им. В.А. Стеклова АН СССР, 1968, Т.98. С.26 - 87.
17. Робинсон
Дж. Машинно — ориентированная логика, основанная на принципе резолюции
//Кибернетический сборник (новая серия). 1970. Вып.7. С.194 - 218.
18. Данцин
Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки
научных семинаров ЛОМИ АН СССР, Т.105. Л., 1981.
19. Катречко С.Л. Модификация обратного метода
С.Ю.Маслова //Материалы Х Всесоюзной конференции по логике, методологии и философии
науки. — Минск, 1990. С.110 - 112.
20. Катречко
С.Л. Моделирование правила расщеплений в обратном методе С.Ю. Маслова //Логические
методы в компьютерных науках. — М.,
ИФРАН, 1992, С. 125 -141.
21. Катречко
С.Л. Обратный метод С. Ю. Маслова //Логика и компьютер (вып.2): логические
языки, содержательные рассуждения и методы поиска доказательства. — М., Наука,
1995. С.62 - 75.
22. Царьков
Д.В., Катречко С.Л. Об одном алгоритме приведения пропозициональных формул к
д. н. ф //Тезисы международной конференции (1-ые) «Смирновские
чтения», Москва, 1997.
23. Царьков
Д.В. Новый алгоритм преобразования формул в Д. Н. Ф //Тезисы международной
конференции «Развитие логики в России: итоги и перспективы», Москва, 1997.
24.
Интеллектуальный бектрекинг //Логические исследования, Вып.3. — М., Наука,
1995.
25. Katrechcko S.L. Frege's system and proof-search theory
//Abstacts of Russian conference "Frege's and Hilbert's heritage in the
XX-th centure: logic, philosophy and mathematics", Kaliningrad, 1992. P.7 - 8.
26. Логика и
компьютер. Вып.3. — М., Наука, 1996.