ПРАВИЛА ВЫВОДА исчисления следующие:

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

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

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

правило ® Ъ ® B, A1 Ъ A2 Ъ … Ъ An, C

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

Построим дерево поиска вывода F, в котором знак “Ъ” по правилу ®Ъ предварительно заменен на "," ):

Д Д

® a, ~a, a&~b, ~b ® a, b, a&~b, ~b

[4] [5]

\ /

\ /

\ /

Д !

® a, ~a&b, a&~b, ~a ® a, ~a&b, a&~b, ~b

[2] [3]

\ /

\ /

\ /

!

®a, ~a&b, a&~b, ~a&~b

[1]

Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком Д), т.е. содержат контрарную пару литер: a и ~a — в секвенциях 2 и 4, b и ~b — в секвенции 5. Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции могут быть удалены — "прополоты". Сформулируем алгоритм "прополки" [9], на основании которого преобразуем полученное дерево вывода формулы F. "Избыточными" для 2 секвенции являются формулы a & ~b и ~a & b, для секвенции 4— формула a & ~b и литера ~b, для секвенции 5 — формула a & ~b и литера a. На основании произведенной "прополки" концевых секвенций ветвей "прополем" нижележащие секвенции данной ветви, из которых удаляются литеры и боковые формулы секвенции, не встречающиеся в верхних секвенциях данной ветви. Так как формула a & ~b не встречается в секвенциях 4 — 5 и 2, то она может быть сначала удалена из секвенции 3, и затем, из корневой секвенции 1. "Прополотое" дерево вывода F выглядит так:

® a, ~a ® b, ~b

\ /

\ /

\ /

® a, ~a ® a, ~a&b, ~b

\ /

\ /

\ /

®a, ~a&b, ~a&~b

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

Формула F будет выглядеть так: 10 Ъ 21 & 22 Ъ 31 & 32 Ъ 41 & 42. "Прополотое" дерево вывода будет выглядеть так:

(значение квадратных скобок и знака  будет объяснено ниже)

® 10, 21 ® 22, 42

\ /

\ /

\ /

® 10, 41 ® [10 42], 21 & 22

\ /

\ /

\ /

® , 10, 21 & 22, 41 & 42

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

Введем исчисление чисел с индексами явным образом. Исходное понятие исчисления — понятие набора, который представляет собой множество чисел с индексами. Аксиомами исчисления являются все такие пары чисел с индексами, которые соответствуют контрарным парам литер исходной формулы — исходные благоприятные наборы. Концевые вершины "прополотого" дерева вывода, а также наборы: [21 31], [31 41], [22 32] образуют аксиомы исчисления поиска для формулы F. Единственное правило вывода исчисления позволяет получать новые благоприятные наборы объединением нескольких благоприятных наборов, при котором возможно удаление тех чисел с индексами, которые образуют полную совокупность литер некоторого дизъюнкта. В "прополотом" дереве вывода формулы F вновь полученные благоприятные наборы при движении по дереву "сверху вниз" заключены в квадратные скобки.