2

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

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

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

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

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

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

® 21 51 ® 42 52 ® 22 61 ® 10 62 ® 32 63





(5) (6)

® 21 41 ® [ 21 42 ] ® 22 31 ® [ 22 32 ] ® 10 33





(4) (3)

® 21 ® 22





(2)

® — {1 2 3 4 5 6}

рис.3

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

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

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

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

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



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

Примерами аксиом (по правилу А) формулы Ф являются двухчленные наборы в "прополотом дереве вывода", а также следующие наборы: 52 63, 32 42, 33 71, 62 71

ПРАВИЛО Б (единственное правило вывода данного исчисления, которое задает механизм образования новых благоприятных наборов): если наборы с зависимостями An .