Реферат: Обратный метод С. Ю. Маслова *1*

С.Л. Катречко
Обратный метод С.Ю. Маслова *1*
В 60-е годы можно говорить о возникновении новой области на стыке логики, эвристики, психологии — теории поиска вывода.

Теория поиска вывода (ТПВ) — это область математической логики, которая изучает возможные способы решения задач в каком-либо исчислении. Более точно, согласно работе С.Ю. Маслова "Теория дедуктивных систем и ее применения", проблематику ТПВ можно определить так: выявление по исчислению и объекту в языке этого исчисления структуры возможных выводов этого объекта, причем выводов интересных в каком-либо отношении. Развитие ТПВ тесно связано с развитием ЭВМ и проблематикой "искусственного интеллекта", так как именно исследования в области "искусственного интеллекта" особенно остро поставили вопрос о том, как протекает процесс решения у человека и как научить этому ЭВМ.

Данная статья будет посвящена области ТПВ, которая получила название автоматическое доказательство теорем [1] и имеет тесную взаимосвязь с логическим программированием [2]. В данной статье внимание будет сосредоточено на одном из важных и интересных результатов в этой области — обратном методе, который был предложен в середине 60-ых годов одним из пионеров разработки теории поиска вывода, российским логиком С.Ю. Масловым (1932 — 1983). Полное представление об обратном методе (ОМ) можно получить в оригинальных работах С.Ю. Маслова [см., например, работу 3].

В настоящее время в ТПВ существует несколько мощных методов автоматического доказательства теорем логических исчислений, среди которых наиболее известными и разработанными являются метод резолюций [4] и метод расщеплений [5]. По своим возможностям обратный метод С.Ю. Маслова является не менее эффективным методом автоматического доказательства теорем, но из-за ряда причин не получил широкого распространения в программировании. Одной из причин такого положения дел является сложность понимания ОМ в оригинальном изложении С.Ю. Маслова. В данной статье будет предложена некоторая конкретизация ОМ для исчисления высказываний, которая проясняет "механизм работы" обратного метода. Другое изложение ОМ для исчисления высказываний можно найти в статьях Г.В. Давыдова [6, 7].

Более того, здесь будет сделана попытка представить логические исчисления, построенные на базе обратного метода (исчисления благоприятных наборов), в качестве базисного языка для "подключения" мощных правил вывода и моделирования других методов АДТ, и в частности для моделирования метода резолюций и метода расщеплений.

Для изложения идейной стороны обратного метода в данной статье устанавливается тесная взаимосвязь ОМ с секвенциальными исчислениями. При этом прослеживается "генетическая" зависимость ОМ от секвенциальных исчислений, которая и проясняет суть подхода, предложенного в обратном методе С.Ю.Маслова.
^ ОБРАТНЫЙ МЕТОД И СЕКВЕНЦИАЛЬНЫЕ ИСЧИСЛЕНИЯ
Для формулировки обратного метода С.Ю. Маслова в исчислении высказываний (исчисления благоприятных наборов) и выявления основных идей, заложенных в ОМ, постараемся последовательно воспроизвести путь его формирования из секвенциальных исчислений. Для этого необходимо коснуться существенных особенностей этих исчислений.

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

Секвенциальные исчисления и представляют собой один из возможных способов такого последовательного анализа. В настоящее время существует несколько других исчислений аналитического характера, реализующих эту идею: например, исчисление аналитических таблиц Р. Смульяна [**; 8] или метод семантических таблиц Э. Бэта [9].

Суть работы секвенциальных исчислений сводится к последовательной разбивке исходной формулы на более простые подформулы до тех пор, пока не будут получены элементарные подформулы, по виду которых можно утверждать о выводимости (невыводимости) исходной формулы. Такой "механизм работы" секвенциальных исчислений основан на свойстве подформульности, которое после доказательство Г. Генценом теоремы об устранимости сечения [9] получило универсальный характер.

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

Именно эти особенности секвенциальных исчислений сделали их удобным аппаратом для выполнения "механического" построения выводов: подформульность исчислений гарантирует окончание процесса "расщепления" любой сложной формулы до элементарных подформул, а обратимость правил вывода — превращение "заготовки" вывода при определенных условиях в вывод. С другой стороны, эта машинообразность процедуры поиска приводит к неэффективности поиска вывода и резкому увеличению сложности вывода при увеличении сложности исходных формул. Возникает проблема так называемого экспоненциального взрыва. Связано это с тем, что в секвенциальных исчислениях строится полное дерево поиска вывода "слепым перебором". При этом приходится "проделывать" много лишней работы, которая и ведет, в конечном итоге, к резкому увеличению сложности вывода. "Открытие" этого факта в логике в 70-е годы привело, с одной стороны, к бурному развитию АДТ, в котором пытаются преодолеть неэффективность аналитических исчислений, а с другой стороны, к появлению новой дисциплины — теории сложности, в рамках которой было осознано, что проблема экспоненциального взрыва имеет принципиальный характер и для решения этой проблемы (в общем виде она получила название P = NP — проблемы) необходимы принципиально новые подходы [10].

Одним из возможных подходов к повышению эффективности поиска вывода является идея глобальной обработки информации, которая была предложена в 60-е годы одновременно советским логиком Н.А. Шаниным и шведским логиком С. Кангером. Суть идеи заключается в попытке более полного использования информации о структуре формулы и уже полученного дерева поиска вывода и за счет этого сделать поиск вывода более "разумным".

С одной стороны, при отсутствии необходимой информации предварительно строится некоторая "заготовка" вывода, которую при получении недостающей информации можно либо превратить в вывод, либо отрицательно ответить на вопрос о выводимости данной формулы. Для исчисления предикатов эта идея находит выражение в использовании при поиске вывода новых объектов, метапеременных, которые позволяют без необходимости не конкретизировать вывод при отсутствии достаточной информации [см. ст. С. Кангера в 9].

С другой стороны, используя полученную информация о структуре формулы и уже полученного дерева вывода, можно попробовать исключить из дерева поиска ту информацию, которая является избыточной для построения вывода или дублирует информацию, содержащуюся в других частях дерева поиска. Т.е. при построении дерева поиска вывода использовать "глобальную" информацию всего дерева. Это направление идеи "глобальной обработки информации" получило развитие в работах группы ленинградских логиков под руководством Н.А. Шанина [11].

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

Во-первых, получила дальнейшее развитие идея анализа информации, заключенной в исходной формуле. Исчисления обратного метода строятся для каждой конкретной формулы, которую необходимо доказать. По виду исходной формулы, в понятии исходного благоприятного набора, определяется вид только тех аксиом, которые могут быть "полезны" для построения вывода данной формулы. Все остальное бесконечное множество аксиом не используется.

Во-вторых, в обратном методе существенным образом используется обратимость правил секвенциальных исчислений: так как правила поиска вывода, применяемые "снизу вверх" при поиске, могут быть использованы "сверху вниз" при построении дерева вывода, то возможно создание "универсального" механизма построения дерева вывода "сверху вниз" - правило Б обратного метода. Тем самым, обратный метод еще раз "перевернул" направление построения дерева вывода по сравнению с секвенциальными исчислениями. Именно с этим обращением направления поиска и связано название обратного метода.

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

Технически такие исчисления в данной статье построены для формул исчисления высказываний в дизъюнктивной нормальной форме.
^ ОБЩАЯ СХЕМА ОБРАТНОГО МЕТОДА
Пусть нам дана некоторая формула Ф в дизъюнктивной нормальной форме, где графически равные дизъюнкты и конъюнкты сокращены до одного, и секвенциальное исчисление, в котором необходимо установить выводимость данной формулы. Так как формула Ф находится в дизъюнктивной нормальной форме, то секвенциальное исчисление содержит лишь одно ПРАВИЛО ВЫВОДА:

n–кратное  B, A1, C;  B, A2, C; …  B, An, C;

правило  &  B, A1 & A2 & … & An, C

Для полноты исчисление содержит еще одно правило — n-кратное правило  . Однако применение n-кратного правило   (применение его "сверху вниз") и соответственно контрприменение правила (применение правила "снизу вверх") при данном типе формул является тривиальным: все запятые (,) можно просто заменить знаками дизъюнкции () во всей формуле Ф (соответственно, при контрприменении правила — наоборот). Условимся, что тривиальное n-кратное правило   будет применяться автоматически в самом начале поиска вывода любой формулы. Заметим, что правило сечения является допустимым для введенного секвенциального исчисления, а структурные правила избыточны.

АКСИОМАМИ данного исчисления являются секвенции вида  A, X, ~X, B, которые содержат контрарную пару литер.

ВЫВОДОМ формулы Ф называется дерево, полученное применением правил вывода, в концевых вершинах которого стоят аксиомы, а в корне дерева — формула Ф.

Пусть ^ Ф = ~c  b&a  ~a&d&c  ~b&~d  ~b&d  ~a&c&~d  ~c&x&y (или

~c  ba  ~adc  ~b~d  ~bd  ~ac~d  ~cxy, где знак & опущен)

Построим некоторое дерево поиска вывода данной Ф формулы в сформулированном секвенциальном исчислении. Начинаем построение дерева с исходной формулы Ф. Используя свойство обратимости правил вывода, сначала контрприменяем правило  , а потом — последовательно — правило  &. Строим дерево поиска вывода снизу вверх (см. рис.1), последовательно "расщепляя" дизъюнкты формулы Ф до литер (расщепляемые дизъюнкты обозначены в квадратных скобках). Продолжаем этот процесс построения дерева до тех пор, пока в узлах дерева не будет получена контрарная пара литер (этот узел помечается знаком ) или во всех концевых вершинах дерева останутся только литеры формулы Ф (в этом случае формула Ф — невыводима):

  

~c, a, d, ~b~d, ~bd, ~a, …  ~c, a, d, ~b~d, ~bd, c, …  ~c, a, d, ~b~d, ~bd, ~d, …


 [6] 

 ~c, a, ~a, …  ~c, a, d, ~b~d, ~bd, ~ac~d, ~cxy  ~c, a, c, …




 

~c, b, ~adc, ~d, ~b, …  ~c, b, ~adc, ~d, d, …


 [5]

~c, b, ~adc, ~b, …  ~c, b, ~adc, ~d, ~bd, ~ac~d, ~cxy [3]


[4]

 ~c, b, ~adc, ~b~d, ~bd, ~ac~d, ~cxy  ~c, a, ~adc, ~b~d, ~bd, ~ac~d, ~cxy



[2]

 ~c, ba, ~adc, ~b~d, ~bd, ~ac~d, ~cxy

рис.1

Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком ), т.е. содержат контрарную пару литер, например: a и ~a — в секвенциях 3 (лев.) и 6 (лев.), b и ~b — в секвенции 4 (лев.). Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции несущественны и помечены многоточием. Так как все концевые вершины дерева поиска вывода представляют аксиомы исчисления (помечены знаком ), то получен вывод формулы Ф.

Отметим несколько особенностей полученного дерева вывода:

Во всех концевых вершинах содержатся только те литеры (возможно "нерасщепленные" дизъюнкты), которые принадлежат исходной формуле Ф, причем если Ф выводима, то во всех концевых вершинах содержатся контрарные пары литер.

Нет необходимости продолжать "расщепление" дизъюнктов формулы дальше, если получена хоть одна контрарная пара литер.

Правило вывода  & при контрприменении действует локально, т.е. добавляет на каждом уровне построения дерева лишь одну новую в каждую ветвь дерева.

При построении дерева поиска вывода были использованы некоторые интуитивные соображения: например, нецелесообразно работать ("расщеплять") с последним дизъюнктом формулы Ф, в составе которого встречаются литеры Х и У, так как эти литеры ни в каких дизъюнктах больше не встречаются. Видимо, более целесообразно работать с теми дизъюнктами, которые лучше "зацеплены" с другими дизъюнктами.

При построении дерева поиска приходится записывать много излишней информации, которая либо уже содержится в корневой секвенции дерева (переписывание "нерасщепленных" дизъюнктов в каждом узле дерева), либо является излишней для превращения какого-либо узла дерева в аксиому: все те литеры, которые не составляют контрарной пары в этих узлах (собственно этот пункт мы уже частично учли, когда помечали ненужные члены многоточием — см. рис.1).

Для удаления из полученного дерева вывода избыточной при построения вывода информации представим исходную формулу Ф и полученный вывод в виде чисел с индексами следующим образом. Каждому дизъюнкту исходной формулы поставим в соответствие порядковый номер этого дизъюнкта в формуле (число без индекса), а каждой литере — число с индексом, где число обозначает номер дизъюнкта, а индекс - порядковый номер данной литеры в этом дизъюнкте. Если дизъюнкт состоит из одной литеры, то литера этого дизъюнкта получает в качестве кода число с индексом ноль. Тогда Ф будет выглядеть так: 10 2122 313233 4142 5152 616263 717273

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

Полученное дерево вывода с учетом кодировки и исключением из записи запятых будет выглядеть так (см. рис.2)

  

 1 22324 5 617  1 22324 5 627  1 22324 5 637


 (6) 

 1 22314 5 6 7  1 22324 5 6 7  1 22334 5 6 7

 

1 213 42516 7  1 213 42526 7


 (5)

1 213 415 6 7  1 213 425 6 7


(4) (3)

 1 213 4 5 6 7  1 223 4 5 6 7



(2)

 1 2 3 4 5 6 7

рис.2

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

Сформулируем алгоритм "прополки" числового дерева вывода:

1. В каждой концевой вершине (аксиоме) вычеркнем все числа без индексов и числа с индексами, которые не образуют контрарных пар. Заметим, что этот процесс вычеркивания однозначен, поскольку секвенциальное исчисление локально и при получении первой контрарной пары заканчивает свою работу.

2. Из узлов дерева последовательно сверху вниз вычеркнем все числа (с индексами и без индексов), не встречающиеся вверху в некотором наследнике данного узла (наследником считается узел, полученный из данного при построении дерева поиска вывода при контрприменении правила  &).

Этот процесс прополки продолжается сверху вниз во всех ветвях дерева вывода от концевых вершин к корню дерева. Причем, если во всех наследниках узла содержатся числа с индексами, а в самом узле "появилось" это число без индекса, то запишем его рядом с этим узлом в круглых скобках. Содержательно это соответствует контрприменению правила  & к дизъюнкту под этим номером.

Применим алгоритм "прополки" к числовому дереву вывода Ф (см. рис.3):

 2151 4252 2261 1062 3263




(5) (6)

 2141 [ 2142]  2231 [ 2232]  1033




(4) (3)

 21 22




(2)

  {1 2 3 4 5 6}

рис.3

Получим "прополотое дерево вывода", где концевым вершинам поставлены в соответствие двухчленные множества из чисел с индексами. Так как концевые вершины дерева вывода являются аксиомами, то по алгоритму прополки данные числа с индексами в концевых вершинах соответствуют некоторой контрарной паре литер исходной формулы. Узлам дерева вывода соответствуют конечные множества чисел с индексами, "расщепляемым" по правилу  & (для наглядности они помечены квадратными скобками). "Расщепляемым" дизъюнктам исходной формулы — числа без индексов в круглых скобках. В корне дерева записана пустое множество, рядом с которым в фигурных скобках записаны номера всех дизъюнктов исходной формулы:

Полученное после прополки дерево является примером дерева вывода Ф в исчислении благоприятных наборов.

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

НАБОРОМ называется последовательность чисел с индексами, где графически равные члены сокращаются до одного и порядок записи чисел с индексами несущественен. Набор записывается в строчку без скобок.

^ НАБОРОМ С ЗАВИСИМОСТЬЮ называется набор, справа от которого в круглых скобках приписана некоторая последовательность чисел без индексов (в зависимости порядок записи числе также несущественен и графически равные члены сокращаются до одного).

<понятие набора с зависимостью по существу понадобится только для моделирования правила расщепления — см. конец данного текста, — а для ближайшего изложения можно ограничиться исчислением благоприятных наборов без зависимостей, т.е. словосочетание «с зависимостью» просто исключить из ближайшего текста. Хотя содержательный смысл введенного понятия «зависимости» тривиален: это получаемые дизъюнкты при построении секвенциального дерева. В частности на рис.3 (конечная) зависимость исходной формулы Ф приведена в фигурных скобках, причем можно обратить внимание, что в ней отсутствует дизъюнкт (число) 7, поскольку он не был получен при построении секвенциального дерева.>

^ ПРАВИЛО А (задает базис исчисления): если двухчленный набор с зависимостью содержит два числа с индексами, которые соответствуют контрарной паре литер, то такой набор с зависимостью называется исходным благоприятным набором. Зависимость исходных благоприятных наборов пустая (круглые скобки справа вообще не пишутся).

Примерами аксиом (по правилу А) формулы Ф являются двухчленные наборы в "прополотом дереве вывода", а также следующие наборы: 5263, 3242, 3371,6271

^ ПРАВИЛО Б (единственное правило вывода данного исчисления, которое задает механизм образования новых благоприятных наборов): если наборы с зависимостями An ... B1 (X, …) ,..., Сm ... Вp (У, …) являются благоприятными наборами с зависимостями и B1, ..., Вp составляют полную совокупность литер некоторого дизъюнкта исходной формулы (дизъюнкта под номером B), то набор с зависимостью Аn … Сm … (Х, .., У, .., B) также является благоприятным (в зависимость этого набора добавляется номер B).

^ Тривиальным применением правила Б называется перенесение числа с индексом ноль в зависимость этого набора (уже без индекса).

Правило Б позволяет получать новые благоприятные наборы, из состава которых исключены те числа с индексами, которые образуют полную совокупность всех чисел с индексами некоторого числа без индекса.

Примерами "новых" благоприятных наборов полученных по правилу Б являются множества в квадратных скобках в "прополотом дереве вывода" (см. рис.3), а также следующие наборы: [33] — получен из исходного благоприятного набора 1033 тривиальным применением правила Б); [62] — получен из исходного благоприятного набора 1062 тривиальным применением правила Б); [21 63] — получен из исходных благоприятных наборов 21 51 и 63 52, так как 52 и 52 образуют дизъюнкт 5 формулы Ф; [22 42] — получен из благоприятных наборов 32 42, 22 31, [33], так как числа 31, 32и 33 образуют полную совокупность литер третьего (3) дизъюнкта Ф.

ВЫВОДОМ называется линейная последовательность благоприятных наборов с зависимостями, последним членом которой является пустой (нольчленный) благоприятный набор (на рис.3 он обозначен знаком ).

Примером вывода исчисления благоприятных наборов является полученное по алгоритму прополки "прополотое дерево вывода" на рис.3.

Другим примером вывода является следующая линейная последовательность наборов с анализом. Под анализом будем понимать указание около каждого "нового" благоприятного набора его предшественников, т.е. номеров тех строчек, из которых получен данный набор.

1. 10338. 2261

2. [33] из 1 9. [22] из 5, 7, 8

3. 3263 10. 2151

4. 312211. 4252

5. [2263] из 2, 3, 4 12. [2142] из 10, 11

6. [1062] 13. 2141

7. [62] из 6 14. [21] из 12, 13

15.  из 9, 14

Для того чтобы быть уверенным, что построенное исчисление благоприятных наборов является эквивалентным исходному секвенциальному исчислению сформулируем теорему о полноте:

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

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

В обратную сторону, теорема следует из того, что при наличии вывода в исчислении благоприятных наборов мы по крайней мере дважды должны применить правило Б для получения пустого благоприятного набора. Но любое применение правила Б соответствует "получению" в секвенциальном выводе некоторого дизъюнкта исходной формулы Ф. При этом возможно получение не всех дизъюнктов исходной формулы. Например, для приведенной формулы Ф правило Б не будет применяться к литерам дизъюнкта под номером 7 (к числам с номером 7), а это значит, что будет получен вывод более сильной формулы Ф* без последнего дизъюнкта формулы Ф. Значит при получении пустого набора будет получено доказательство формулы Ф*, которая не слабее формулы Ф. Теорема доказана.

Таким образом, полученное исчисление, с одной стороны, эквивалентно в смысле выводимости исходному секвенциальному исчислению и позволяет "кодировать" выводы целого класса формул определенной структуры. Благодаря анализу информации о структуре формулы и учету особенностей построения секвенциальных выводов удалось частично избавиться от "слепого перебора", характерного для секвенциальных исчислений. Построение выводов стало более осмысленным.

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

Возможны следующие подходы решения проблемы повышения эффективности предложенной "заготовки" исчисления:

1. Модификация предложенной схемы за счет "подключения" различного рода эвристик и допустимых правил вывода, которые повышают мощность первоначальной "заготовки" исчисления. В этом случае "сфера действия" правила Б расширяется.

2. Модификация предложенного исчисления за счет ограничения числа благоприятных наборов, участвующих в выводе. В данном случае "сфера действия" правила Б ограничивается.

Отметим, что данные подходы противоречат друг другу, но лишь отчасти.
^ МОДИФИКАЦИИ ОБЩЕЙ СХЕМЫ ОБРАТНОГО МЕТОДА.
МОДЕЛИРОВАНИЕ ПРАВИЛА РЕЗОЛЮЦИЙ


Как было отмечено выше, исчисления благоприятных наборов являются удобным базисом для моделирования различных правил вывода и эвристик, соответствующим разным методам автоматического теорем. Как известно из литературы [12], важным средством повышения мощности (эффективности) систем поиска вывода является моделирование в них правила сечения. Для сформулированного выше секвенциального исчисления правило сечения является допустимым. Сравним правило сечения с правилом Б исчисления благоприятных наборов. Для этого запишем их следующим образом:

правило вывода Б исчисления правило сечения

 A, X  B, Y  A, C  B, ~C

 A, B, X & Y  A, B, C & ~C

 A, B (F)  A, B

Здесь X & Y можно исключить правилу Здесь C & ~C можно исключить по правилу

вывода исчисления, при условии, что сечения, так как ^ C & ~C — противоречие и его

X & Y образуют формулы Ф. удаление не нарушает выводимости  A, B

Как видно из приведенного рисунка "механизм работы" этих двух правил аналогичен, т.е. налицо структурное сходство. Правило Б можно понимать как аналог правила сечения, который при своем применении сверху вниз, также как и правило сечения позволяет исключать некоторые литеры, которые встречались в верхней части правил. Если правило сечения исключает те литеры, которые образуют контрарные пары, то правило Б — литеры, которые образуют некоторый дизъюнкт исходной формулы Ф. И в том, и в другом случае преобразования сохраняют эквивалентность формул.

Для моделирования правила сечения можно предложить следующую модификацию правила Б:

^ ПРАВИЛО Б*: При образовании благоприятных наборов разрешено выбрасывать не только те числа с индексами, которые составляют полную совокупность по некоторому числу, но и те числа с индексами, которые образуют один из исходных благоприятных наборов.

"Сфера действия" двухпосылочного правила Б расширяется: теперь при "склеивании" благоприятных наборов разрешается выбрасывать контрарные пары литер. Такая модификация правила Б и соответствует моделированию правила сечения относительно формулы Ф, поскольку применение правила Б по некоторому исходному благоприятному набору и соответствует выбрасыванию из состава формулы контрарных пар литер. При этом, возможности исходного исчисления расширяются. Теперь эти исчисления можно использовать для установления ложности формул: если при построении вывода применять правило Б только по исходным благоприятным наборам, то получение пустого благоприятного набора позволяет сделать вывод о том, что в составе исходной формулы Ф содержатся только противоречивые дизъюнкты и, следовательно, формула Ф тождественно — ложна. Для сохранения теоремы о полноте исчисления необходимо потребовать хотя бы однократного применения правила Б в старой формулировке (применение правила Б по некоторому числу). Более строгое доказательство такой модификации дано в [13].

При внимательном рассмотрении схемы правила сечения, можно утверждать, что при применении "сверху вниз" правило сечения соответствует правилу резолюций: здесь также при "смешивании" двух дизъюнктов получается новый дизъюнкт за счет выбрасывания контрарной пары литер. Таким образом, получился своеобразный синтез обратного метода с методом резолюций.

Другим направлением модификации предложенного исчисления является минимизации числа благоприятных наборов, участвующих в выводе. Например, из приведенного анализа дерева вывода (смотри п.5 анализа после рис.1) напрашивается следующая модификация исчисления:
ЛЕММА 1
Если в некотором исходном благоприятном наборе встречается число с индексом такое, что полной совокупности индексов по данному числу нет, то все такие наборы без потери выводимости можно исключить из числа исходных благоприятных наборов.

Доказательство леммы очевидно: если правило Б в процессе построения вывода применяется к некоторому такому набору, то пустой благоприятный набор получить нельзя.

В нашем примере, без потери выводимости можно исключить следующие исходные благоприятные наборы 3371 и 6271

На основании леммы 1 возможно "подключить" к предложенной выше схеме исчисления следующую модификацию:
ЛЕММА 2
Если в составе исходных благоприятных наборов встречаются наборы, содержащие числа с индексом ноль, то все такие наборы, без потери выводимости, можно вычеркнуть, изменив индексацию других чисел этих наборов в остальных исходных благоприятных наборах.

Формулировка этой леммы основана на моделировании в исчислении известном для систем поиска вывода правила исключения однолитерных дизъюнктов: если в составе формулы встречается однолитерный дизъюнкт, то его можно без потери выводимости вычеркнуть из формулы, одновременно исключив из других дизъюнктов этой формулы литеры, контрарные литере этого однолитерного дизъюнкта [4]. Доказательство корректности этой леммы можно получить из допустимости правила исключения однолитерных дизъюнктов в секвенциальном исчислении.

Для минимизации числа "новых" благоприятных наборов, полученных по правилу Б можно предложить следующую лемму, которую можно назвать леммой о нормализации вывода:
ЛЕММА 3
При наличии среди уже имеющихся благоприятных наборов такого благоприятного набора, который является подмножеством некоторого вновь полученного благоприятного набора, использование этого нового благоприятного набора для получения вывода избыточно.

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