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

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

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

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

Д Д Д

® 1 22 32 4 5 61 7 ® 1 22 32 4 5 62 7 ® 1 22 32 4 5 63 7



Д (6) Д

® 1 22 31 4 5 6 7 ® 1 22 32 4 5 6 7 ® 1 22 33 4 5 6 7

Д Д

® 1 21 3 42 51 6 7 ® 1 21 3 42 52 6 7



Д (5)

® 1 21 3 41 5 6 7 ® 1 21 3 42 5 6 7



(4) (3)

® 1 21 3 4 5 6 7 ® 1 22 3 4 5 6 7





(2)

® 1 2 3 4 5 6 7

рис.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

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