Cтраница 3
По лемме 5.1 существует такая резольвента С из С и С2, что С - основной пример С. Пусть Т - - замкнтое семантическое дерево для ( Su C), полученное из Т вычеркиванием любого узла или ребра, которое находится ниже первого узла, где резольвента С опровергается. Подставляя эту резольвенту в ( 5и С), мы си-ожем получить другое замкнутое семантическое дерево с меньшим числом узлов. [31]
Когда эрбрановский базис множества S бесконечен, всякое полное семантическое дерево для S будет тоже бесконечно. Легко видеть, что полное семантическое дерево для S соответствует исчерпывающему перебору всех возможных интерпретаций для S. Если S невыполнимо, то S не сможет быть истинным в каждой из этих интерпретаций. Таким образом, мы можем остановить рост дерева из узла N, ести / ( N) опровергает S. Это порождает следующие определения. [32]
Таким образом, все возможные случаи приводят к тождественно истинным формулам. На рис. 7.2 а изображено семантическое дерево, соответствующее формуле / з, а на рис. 7.26 показана часть семантического дерева, которая фактически использовалась для проверки общезначимости. [33]
Поскольку каждая ветвь Т имеет опровергающий узел, то существует замкнутое семантическое дерево Т для S. Таким образом, мы заканчиваем доказательство первой половины теоремы. [34]
Как можно увидеть, эти два дизъюнкта должны иметь контрарную пару литер и, следовательно, могут служить посылками правила резолюций. Если мы добавим в S дизъюнкт - Р, то мы будем иметь замкнутое семантическое дерево Т для SU - P, показанное на рис. 9, с. На рис. 9, с узел ( 1) - выводящий узел. [35]
Понятие псевдосемантического дерева может быть использовано для нахождения решения данного якобы П - противоречивого множества М для некоторого множества 5 дизъюнктов. Если М содержит только основные дизъюнкты, то замкнутое псевдосемантическое дерево, а в действительности замкнутое семантическое дерево может быть легко найдено следующим образом. Начинаем с верхнего узла. Выращиваем два ребра, исходящих из верхнего узла. Приписываем одному из этих узлов литеру А, другому - А. Если имеется, то N - опровергающий узел, и помечаем его крестиком X. В противном случае N не является опровергающим узлом. В этом случае выращиваем из N два ребра. Этот процесс повторяется снова и снова до тех пор, пока все концевые узлы не станут опровергающими узлами. Если это произошло, окончательное дерево является замкнутым семантическим деревом. [36]
По теореме Эрбрана ( теорема 4.3) множество S дизъюнктов является противоречивым тогда и только тогда, когда имеется конечное замкнутое семантическое дерево для S. [37]
Таким образом, все возможные случаи приводят к тождественно истинным формулам. На рис. 7.2 а изображено семантическое дерево, соответствующее формуле / з, а на рис. 7.26 показана часть семантического дерева, которая фактически использовалась для проверки общезначимости. [38]
Как было отмечено ранее, мы сами выбираем порядок выбора очередного элемента из Н для подстановки в атомы из множества S. Например, если мы выберем Q ( f ( a)) сразу вслед за Р ( а), мы получим очень простое семантическое дерево Т2 для множества S, в котором все ветви противоречивы. [39]
В главе 4 мы представили понятие семантических деревьев для доказательства теоремы Эрбрана. Действительно, существует тесная связь между семантическим деревом и резолютивным выводом, что демонстрируется следующим примером. [40]
Это множество S также невыполнимо. Однако нелегко обнаружить вручную конечное невыполнимое множество S основных примеров дизъюнктов множества S. Один путь нахождения такого множества S состоит в порождении замкнутого семантического дерева Т для S. Тогда множество S всех основных примеров, опровергаемых во всех опровергающих узлах Г, и есть искомое множество. Это множество S приводится ниже. Читатель может проверить, что каждый основной дизъюнкт в S есть основной пример некоторого дизъюнкта множества S и что S невыполнимо. [41]
По лемме 5.1 существует такая резольвента С из С и С2, что С - основной пример С. Пусть Т - - замкнтое семантическое дерево для ( Su C), полученное из Т вычеркиванием любого узла или ребра, которое находится ниже первого узла, где резольвента С опровергается. Подставляя эту резольвенту в ( 5и С), мы си-ожем получить другое замкнутое семантическое дерево с меньшим числом узлов. [42]
Таким образом, корень будет помечен пустым дизъюнктом. Наконец, по построению каждый дизъюнкт является элементом 5 или получен из 5 с помощью резолюции. Число резольвент, которые надо вычислить для установления невыполнимости множества дизъюнктов S, не больше числа невисячих узлов семантического дерева. Тем самым показано, что резолюция неэффективна, если применяется только что описанная простая стратегия. [43]
Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли S пустой дизъюнкт П - Если S содержит Q, то S невыполнимо. Если S не содержит П, то проверяется следующий факт: может ли П быть получен из S. Будет ясно позднее, что по теореме Эрбрана ( вариант I) проверка получения Q эквивалентна подсчету числа узлов замкнутого семантического дерева для S. По теореме 4.3 S невыполнимо тогда и только тогда, когда существует конечное замкнутое семантическое дерево Т для S. Ясно, что S содержит П тогда и только тогда, когда Т состоит только из одного узла - корневого узла. [44]
Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли S пустой дизъюнкт П - Если S содержит Q, то S невыполнимо. Если S не содержит П, то проверяется следующий факт: может ли П быть получен из S. Будет ясно позднее, что по теореме Эрбрана ( вариант I) проверка получения Q эквивалентна подсчету числа узлов замкнутого семантического дерева для S. По теореме 4.3 S невыполнимо тогда и только тогда, когда существует конечное замкнутое семантическое дерево Т для S. Ясно, что S содержит П тогда и только тогда, когда Т состоит только из одного узла - корневого узла. [45]