Ю. Маслова. В данной статье будет предложена некоторая конкретизация ОМ для исчисления высказываний, которая проясняет "механизм работы" обратного метода. Другое изложение ОМ для исчисления высказываний можно найти в статьях Г.В. Давыдова [6, 7].

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

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

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

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

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

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

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

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