)

Множество вершин дерева, заключенных между двумя горизонтальными чертами, назовем уровнем дерева троек. Нумерация уровней начинается с корня дерева, которому присвоен нулевой уровень. Понятие пути изменится следующим образом: путем в дереве назовем последовательность вершин по одной из каждого уровня дерева троек.

На основе исходного исчисления с условной дизъюнкцией сформулируем исчисление поиска на деревьях троек (данное исчисление строится аналогично исчислениям обратного метода С. Маслова [5].

Основой исчисления являются деревья троек, сопоставленные формулам исчисления с условной дизъюнкцией. Из этого следует, что каждой вершине дерева сопоставлены либо переменная, либо константа некоторой формулы исходного исчисления.

Аксиомами исчисления являются концевые вершины с константой t.

Очевидно, что если все концевые вершины дерева являются аксиомами, то формула исходного исчисления, которой сопоставлено данное дерево троек, является тавтологией. Но условия, при которых дерево троек соответствует тавтологии можно ослабить, так как не обязательно требовать наличия среди всех концевых вершин константы t (например, приведенные выше деревья тавтологичных формул содержат среди концевых вершин константу f). Поэтому вводится следующее правило обхода деревьев — правило вывода исчисления, — которое определяется смыслом связки условной дизъюнкции, а именно: если дано поддерево, соответствующее формуле [A, B, C] и известна "направленность" формулы B, то, если B "истинно", т.е. направлено "вправо" — следует A, а в случае противоположной "направленности" B (B — "ложно", т.е. направлено "влево") — следует C.

После вершины t (f) выделенным направлением обхода является направление влево (вправо). После вершины, сопоставленной некоторой переменной возможно либо левое, либо правое направление движения по дереву (эти направления называется противоположными направлениями). Если при движении по дереву после переменной, было выбрано направление вправо (влево), то это направление обхода является выделенным по этой переменной для любого пути, содержащего эту вершину (для отрицания переменной выделяется противоположное направление). Путь с выделенным направлением обхода для каждой вершины называется выделенным путем.

Понятие вывода исчисления, соответствующее тавтологичности исходных формул исчисления высказываний, формулируется так:

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

Очевидно, что закрытые деревья сопоставлены формулам исходного исчисления, которые являются тавтологиями. Например, приведенное выше дерево троек для формулы [pqt, p, t] является выводом исчисления, так как любой путь от корня к концевым литерам этого дерева закрыт (отметим, что после верхней литеры p нельзя выбрать путь вправо к константе f, так как ранее, от корня дерева, было выбрано направление обхода дерева после литеры p влево, а направление обхода после корневой литеры p вправо оканчивалось константой t). Поэтому задачей исчисления поиска является проверка закрытости путей дерева троек.

Правило вывода позволяет сформулировать следующий алгоритм поиска вывода, который является аналогом метода расщепления:

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

Рассмотрим "доказательство" тавтологичности формулы p Й ШШ p. Пусть дано следующее дерево троек:

t f

P t
____________________________________

f t
____________________________________

Ш P

Если мы от корня дерева (на нулевом уровне) выбираем направление влево по ШШ p, то после константы f путь закрыт, поэтому проверяем выделенное направление по ШШ p "вправо" (соответственно для p выделенным направлением является направление "влево"). Так как этот путь также закрыт, то дерево закрыто — формула p Й ШШp тавтологична (в данном случае была использована тактика поиска "снизу вверх", однако возможно использование и других тактик поиска).

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

ПРИМЕЧАНИЕ:

— исчисления поиска вывода относятся к особому классу логических систем, называемых логико-эвристическими системами, в которых помимо "логической" компоненты можно выделить и "эвристическую" компоненту [3, 4]. Для более четкого разделения "логической" и "эвристической" компоненты логических систем возможен следующий подход, предложенный в [5].