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



Д Д Д

® ~c, a, d, ~b~d, ~bd, ~a, … ® ~c, a, d, ~b~d, ~bd, c, … ® ~c, a, d, ~b~d, ~bd, ~d, …







Д [6] Д

® ~c, a, ~a, … ® ~c, a, d, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, c, …







Д Д

® ~c, b, ~adc, ~d, ~b, … ® ~c, b, ~adc, ~d, d, …



Д [5]

® ~c, b, ~adc, ~b, … ® ~c, b, ~adc, ~d, ~bd, ~ac~d, ~cxy [3]



[4]

® ~c, b, ~adc, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, ~adc, ~b~d, ~bd, ~ac~d, ~cxy





[2]

® ~c, ba, ~adc, ~b~d, ~bd, ~ac~d, ~cxy

рис.1

Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком Д), т.е. содержат контрарную пару литер, например: a и ~a — в секвенциях 3 (лев.) и 6 (лев.), b и ~b — в секвенции 4 (лев.). Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции несущественны и помечены многоточием. Так как все концевые вершины дерева поиска вывода представляют аксиомы исчисления (помечены знаком Д), то получен вывод формулы Ф.

Отметим несколько особенностей полученного дерева вывода:

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

2. Нет необходимости продолжать "расщепление" дизъюнктов формулы дальше, если получена хоть одна контрарная пара литер.

3. Правило вывода ® & при контрприменении действует локально, т.е. добавляет на каждом уровне построения дерева лишь одну новую в каждую ветвь дерева.

4. При построении дерева поиска вывода были использованы некоторые интуитивные соображения: например, нецелесообразно работать ("расщеплять") с последним дизъюнктом формулы Ф, в составе которого встречаются литеры Х и У, так как эти литеры ни в каких дизъюнктах больше не встречаются. Видимо, более целесообразно работать с теми дизъюнктами, которые лучше "зацеплены" с другими дизъюнктами.

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



Д