Cтраница 4
По теореме Эрбрана ( теорема 4.3) множество S дизъюнктов является противоречивым тогда и только тогда, когда имеется конечное замкнутое семантическое дерево для S. Иными словами, мы можем определить псевдосемантические деревья и доказать противоречивость S, породив замкнутое псевдосемантическое дерево. Псевдосемантическое дерево должно удовлетворять меньшему количеству условий, чем семантическое дерево, поэтому его обычно легче строить. [46]
Понятие псевдосемантического дерева может быть использовано для нахождения решения данного якобы П - противоречивого множества М для некоторого множества 5 дизъюнктов. Если М содержит только основные дизъюнкты, то замкнутое псевдосемантическое дерево, а в действительности замкнутое семантическое дерево может быть легко найдено следующим образом. Начинаем с верхнего узла. Выращиваем два ребра, исходящих из верхнего узла. Приписываем одному из этих узлов литеру А, другому - А. Если имеется, то N - опровергающий узел, и помечаем его крестиком X. В противном случае N не является опровергающим узлом. В этом случае выращиваем из N два ребра. Этот процесс повторяется снова и снова до тех пор, пока все концевые узлы не станут опровергающими узлами. Если это произошло, окончательное дерево является замкнутым семантическим деревом. [47]