Семантические деревья. Теорема Эрбрана
Множества H(S), A¢, F¢, у всех Н — интерпретаций сов-падают. Различаются только значения предикатов, которые могут быть либо равны атомам из эрбрановского базиса А, либо противоположны им. Каждый атом Аi Î А входит в одну интерпретацию один раз — либо как Аi, либо как Ø Аi. Пара Аi и Ø Аi называется контрарной.
Рассмотрим для некоторого множества дизъюнктов S эpбрановский базис А = (А1 , А2 . ).
Определение. Полным семантическим деревом Т(S) множества дизъюнктов S называется растущее вниз бинар-ное дерево, в котором из самой верхней вершины — корня (узел 0 -го уровня) выходит пара рёбер А1 и ØА1, из каждого узла i -го уровня — пара рёбер Аi и Ø Аi.
Определение. Путь, включающий в себя по одному узлу каждого уровня i (i =0,1,2,. ), называется ветвью.
Очевидно, при счетном эрбрановском базисе число уровней дерева Т(S) и длина ветвей в нем (число узлов) счетны. Каждая ветвь в Т(S) задаёт одну Н – интерпре-тацию, а все дерево описывает полное множество Н -интер-претаций множества дизъюнктов S.
Пример 1. Построить полное семантическое дерево Т(S) для множества дизъюнктов S = , рассмотренного в Примере 7 п. 6.3.
Решение. Эрбрановский базис A = имеет счётное число эле-ментов. Обозначая отрицание через ~, полное семантичес-кое дерево Т(S) можно представить в следующем виде:
Для определенности все узлы в Т(S) пронумеруем сле-дующим образом: корню присваиваем номер 0, узлам пер-вого уровня (слева направо) — номера 1,2; узлам второго уровня (слева направо) — номера 3,4,5,6;. ; узлам i -го уровня – номера 2 i -1, 2 i , 2 i +1. 2 i+1 -2 и т.д.
Рассмотрим полное семантическое дерево Т(S), соот-ветствующее некоторой невыполнимой формуле В. Если S – множество дизъюнктов, соответствующее В, то это озна-чает, что каждая Н — интерпретация опровергает хотя бы один из его дизъюнктов Di. Поскольку каждый дизъюнкт Di содержит конечное число литер, то его опровержение должно произойти в некотором внутреннем узле полного семантического дерева Т(S).
Определение. Узел j полного семантического дерева Т(S) называется опровергающим, если все интерпретации I(j), содержащие его, опровергают некоторый основной при-мер дизъюнкта Di Î S, а все узлы, лежащие выше j, не опро-вергают ни одного из Di Î S.
Пример 2. Построить полное семантическое дерево Т(S) для множества дизъюнктов S = , выявить опровергающие узлы в нем.
Решение. В данном случае матрица формулы является фор-мулой алгебры логики. Её эрбрановский универсум H(S) = Æ, A¢ = Æ, F¢ = Æ. Эрбрановский базис А=< P, Q, R >. Обозначая отрицание через ~, полное семантическое дере-во можно представить в виде:
Для определённости будем считать, что атомы базиса P = И, Q=И, R=И, а их отрицания — ложны. Тогда
а) узел 2 будет опровергать дизъюнкт D4 = P Î S,
б) узел 4 будет опровергать дизъюнкт D1 =Ø PÚ Q Î S,
в) узел 7 будет опровергать дизъюнкт D2 = Ø Q Ú Ø R Î S,
г) узел 8 будет опровергать дизъюнкт D3 = Ø PÚ R Î S.
Если некоторый узел j полного семантического дере-ва Т(S) является опровергающим, то поддерево, выходящее из него, можно не рассматривать, поскольку все интерпре-тации, проходящие по этим узлам, будут опровергающими. Следовательно, его можно не показывать на схеме.
Определение. Семантическое дерево Тз(S) называется закрытым, если каждая его ветвь заканчивается опровер-гающим узлом.
Семантическое дерево Т(S) в Примере 2 является за-крытым. Для таких деревьев применяют специальные изо-бражения, на которых опровергающие узлы перечёркивают и отбрасывают поддеревья, выходящие из них. Дерево Тз(S) из Примера 2 примет при этом следующий вид:
Теорема Эрбрана. Множество дизъюнктов S невы-полнимо Û когда любому полному семантическому дереву T(S) соответствует конечное закрытое семантическое дерево Тз(S).
Существование закрытого семантического дерева Тз(S) указывает на то, что любая Н — интерпретация приводит к появлению ложных дизъюнктов в S, что эквивалентно опровержимости S.
Алгоритм проверки невыполнимости формул при помощи семантического дерева.
1. Формула В представляется в виде пренексной нормаль-ной формы В¢ с матрицей М в виде конъюнкции дизъ-юнктов.
2. Путем устранения кванторов существования В¢ приво-дится к скулемовской форме, бескванторная часть которой рассматривается как множество дизъюнктов S.
3. Строится эрбрановский универсум H(S) и эрбрановский базис А.
4. Строится семантическое дерево по уровням. В каждом из них производится проверка узлов j на опровержимость (бу-дут ли интерпретации I(j) опровергать хотя бы один дизъ-юнкт Di из S).
Если узел j является опровержимым, то узел отме-чается (обычно — зачеркиванием) и дальнейшее построение дерева из него прекращается.
Если узел j не является опровержимым, то построение дерева из него продолжается.
5. Если на некотором шаге дальнейшее построение дерева оказалось невозможным (поскольку все построенные кон-цевые узлы оказались опровержимыми), то множество дизъ-юнктов S, а, следовательно, и исходная формула В – невы-полнимы.
Если построение семантического дерева продолжает-ся, то на вопрос о невыполнимости S нельзя дать ни поло-жительный, ни отрицательный ответ.
Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:
Источник
6.4. Семантические деревья. Теорема Эрбрана
Множества H(S), A, F, у всех Н — интерпретаций сов-падают. Различаются только значения предикатов, которые могут быть либо равны атомам из эрбрановского базиса А, либо противоположны им. Каждый атом Аi А входит в одну интерпретацию один раз — либо как Аi, либо как Аi. Пара Аi и Аi называется контрарной.
Рассмотрим для некоторого множества дизъюнктов S эpбрановский базис А = ( А1 , А2 , . ).
Определение. Полным семантическим деревом Т(S) множества дизъюнктов S называется растущее вниз бинар-ное дерево, в котором из самой верхней вершины — корня (узел 0-го уровня) выходит пара рёбер А1 и А1 , из каждого узла i -го уровня — пара рёбер Аi и Аi .
Определение. Путь, включающий в себя по одному узлу каждого уровня i ( i =0,1,2, . ), называется ветвью.
Очевидно, при счетном эрбрановском базисе число уровней дерева Т(S ) и длина ветвей в нем (число узлов) счетны. Каждая ветвь в Т(S ) задаёт одну Н – интерпре-тацию, а все дерево описывает полное множество Н-интер-претаций множества дизъюнктов S.
Пример 1 . Построить полное семантическое дерево Т(S ) для множества дизъюнктов S = Q(f(x)), P(a) Q(y)>, рассмотренного в Примере 7 п. 6.3 .
Решение. Эрбрановский базис A = имеет счётное число эле-ментов. Обозначая отрицание через ~, полное семантичес-кое дерево Т(S ) можно представить в следующем виде:
Для определенности все узлы в Т(S) пронумеруем сле-дующим образом: корню присваиваем номер 0, узлам пер-вого уровня (слева направо) — номера1,2; узлам второго уровня (слева направо) — номера 3,4,5,6;. ; узлам i-го уровня – номера 2 i -1, 2 i , 2 i +1, . , 2 i+1 -2 и т.д.
Рассмотрим полное семантическое дерево Т(S), соот-ветствующее некоторой невыполнимой формуле В. Если S – множество дизъюнктов, соответствующее В, то это озна-чает, что каждая Н — интерпретация опровергает хотя бы один из его дизъюнктов Di. Поскольку каждый дизъюнкт Di содержит конечное число литер, то его опровержение должно произойти в некотором внутреннем узле полного семантического дерева Т(S).
Определение. Узел j полного семантического дерева Т(S) называется опровергающим, если все интерпретации I(j), содержащие его, опровергают некоторый основной при-мер дизъюнкта Di S, а все узлы, лежащие выше j , не опро-вергают ни одного из Di S.
Пример 2. Построить полное семантическое дерево Т(S ) для множества дизъюнктов S = P Q, Q R, P R, P>, выявить опровергающие узлы в нем.
Решение. В данном случае матрица формулы является фор-мулой алгебры логики. Её эрбрановский универсум H(S) = , A = , F = . Эрбрановский базис А=< P, Q, R >. Обозначая отрицание через ~, полное семантическое дере-во можно представить в виде:
Для определённости будем считать, что атомы базиса P = И, Q=И, R=И, а их отрицания — ложны. Тогда
а) узел 2 будет опровергать дизъюнкт D4 = PS ,
б) узел 4 будет опровергать дизъюнкт D1 = P Q S,
в) узел 7 будет опровергать дизъюнкт D2 = Q R S,
г) узел 8 будет опровергать дизъюнкт D3 = P R S.
Если некоторый узел j полного семантического дере-ва Т(S) является опровергающим, то поддерево, выходящее из него, можно не рассматривать, поскольку все интерпре-тации, проходящие по этим узлам, будут опровергающими. Следовательно, его можно не показывать на схеме.
Определение. Семантическое дерево Тз(S) называется закрытым, если каждая его ветвь заканчивается опровер-гающим узлом.
Семантическое дерево Т(S) в Примере 2 является за-крытым. Для таких деревьев применяют специальные изо-бражения, на которых опровергающие узлы перечёркивают и отбрасывают поддеревья, выходящие из них. Дерево Тз(S) из Примера 2 примет при этом следующий вид:
Теорема Эрбрана. Множество дизъюнктов S невы-полнимо когда любому полному семантическому дереву T(S) соответствует конечное закрытое семантическое дерево Тз(S).
Существование закрытого семантического дерева Тз(S) указывает на то, что любая Н — интерпретация приводит к появлению ложных дизъюнктов в S , что эквивалентно опровержимости S .
Алгоритм проверки невыполнимости формул при помощи семантического дерева.
1. Формула В представляется в виде пренексной нормаль-ной формы В с матрицей М в виде конъюнкции дизъ-юнктов.
2. Путем устранения кванторов существования В приво-дится к скулемовской форме, бескванторная часть которой рассматривается как множество дизъюнктов S.
3. Строится эрбрановский универсум H(S) и эрбрановский базис А.
4. Строится семантическое дерево по уровням. В каждом из них производится проверка узлов j на опровержимость (бу-дут ли интерпретации I(j) опровергать хотя бы один дизъ-юнкт Di из S).
Если узел j является опровержимым, то узел отме-чается (обычно — зачеркиванием) и дальнейшее построение дерева из него прекращается.
Если узел j не является опровержимым, то построение дерева из него продолжается.
5. Если на некотором шаге дальнейшее построение дерева оказалось невозможным (поскольку все построенные кон-цевые узлы оказались опровержимыми), то множество дизъ-юнктов S , а, следовательно, и исходная формула В – невы-полнимы.
Если построение семантического дерева продолжает-ся, то на вопрос о невыполнимости S нельзя дать ни поло-жительный, ни отрицательный ответ.
1.При помощи построения семантического дерева прове-рить невыполнимость следующих множеств дизъюнктов:
Источник