Одним из возможных подходов к повышению эффективности поиска вывода является идея глобальной обработки информации, которая была предложена в 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, где знак & опущен)

Построим некоторое дерево поиска вывода данной Ф формулы в сформулированном секвенциальном исчислении. Начинаем построение дерева с исходной формулы Ф. Используя свойство обратимости правил вывода, сначала контрприменяем правило ® Ъ, а потом — последовательно — правило ® &. Строим дерево поиска вывода снизу вверх (см.