Семантическое дерево

Cтраница 2

Теперь предположим, что 5 не опровергается семантическим деревом. Тогда построение, описанное в нашем алгоритме никогда не закончится. [16]

Когда эрбрановский базис множества S бесконечен, всякое полное семантическое дерево для S будет тоже бесконечно. Легко видеть, что полное семантическое дерево для S соответствует исчерпывающему перебору всех возможных интерпретаций для S. Если S невыполнимо, то S не сможет быть истинным в каждой из этих интерпретаций. Таким образом, мы можем остановить рост дерева из узла N, ести / ( N) опровергает S. Это порождает следующие определения. [17]

Если множество дизъюнктов S невыполнимо, то S опровергается семантическим деревом. [18]

Множество дизъюнктов 5 называется опровергаемым семантическим деревом, если существует семантическое дерево для 5, ветви которого противоречивы. [19]

Мы отметим, что в каждое замкнутое псевдосемантическое дерево вложено некоторое замкнутое семантическое дерево. [20]

По теореме Эрбрана из противоречивости S следует, что S имеет замкнутое семантическое дерево. [21]

Наоборот, если для каждого полного семантического дерева Т для S существует конечное закрытое семантическое дерево, то каждая ветвь Т содержит опровергающий узел. Это означает, что каждая интерпретация опровергает S. Это завершает доказательство второй половины теоремы. [22]

Как будет видно впоследствии, нахождение доказательства для множества дизъюнктов эквивалентно построению семантического дерева. [23]

Множество дизъюнктов S невыполнимо тогда и только тогда, когда каждое полное Е - семантическое дерево имеет конечное закрытое поддерево. [24]

Неполное семантическое дерево. [25]

Для того чтобы определить, выполнима ли формула А, тривиальный - алгоритм требует просмотра некоторого полного семантического дерева, соответствующего ( конечному) множеству высказываний, встречающихся в А. Для каждого листа этого дерева формула А оценивается согласно соответствующей интерпретации. Формула выполнима, если по крайней мере для одного из листьев получается значение И. Этот алгоритм крайне неэффективен: если формула А содержит п различных высказываний, то нужно рассматривать 2 интерпретаций. [26]

Мы отметим, что дерево, изображенное на рис. 53, а, является также и семантическим деревом. [27]

Если Т состоит только из одного ( корневого), узла, то Q должен принадлежать S, поскольку никакой дру-гой дизъюнкт не может опровергаться в корне семантического дерева. Очевидно, в этом случае теорема истинна. [28]

Неполное семантическое дерево. [29]

Бесконечное семантическое дерево полно, если каждая ветвь, выходящая из корня, определяет тотальную интерпретацию. Полное семантическое дерево, соответствующее Р, является конечным тогда и только тогда, когда Р тоже конечно. В противном случае все его ветви бесконечны. [30]

Страницы: 1 2 3 4