13.5. Теорема Эрбрана

Процедура Эрбрана основывается на теореме 13.3, поэтому для проверки невыполнимости множества дизъюнктов S рассматрива­ются только интерпретации над эрбрановским универсумом. Если S ложно при всех интерпретациях над эрбрановским универсумом S, то можно заключить, что S невыполнимо. Так как обычно суще­ствует много, возможно, бесконечное число таких интерпретаций, они выбираются некоторым систематическим способом с использо­ванием семантических деревьев.

Теорема 13.4 (теорема Эрбрана, вариант 1). Множество дизъ­юнктов S невыполнимо тогда и только тогда, когда любому пол­ному семантическому дереву S соответствует конечное замкну­тое семантическое дерево.

Доказательство. Допустим, что S невыполнимо. Пусть Т — полное семантическое дерево для S. Пусть для каждой ветви В дерева Т I_B — множество всех литер, приписанных всем ребрам ветви В. Тогда I_B сеть интерпретация для S. Так как S невыполнимо, то I_B должна опровергать основной пример С дизъюнкта С в S. Однако, так как С конечно, то на В должен существовать опроверга­ющий узел N_B (лежащий на конечном расстоянии от корня). По­скольку каждая ветвь T имеет опровергающий узел, то существует замкнутое семантическое дерево T для S. Далее, так как из каждого узла в T выходит только конечное число ребер, то T должно быть конечным (т.е. число узлов в Т конечно), иначе мы могли бы найти бесконечную ветвь, не содержащую опровергающих узлов. Таким образом, доказательство первой половины теоремы завершено.

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

Теорема 13.5 (теорема Эрбрана, вариант 2). Множество дизъюнктов S невыполнимо тогда и только тогда, когда суще­ствует конечное невыполнимое множество S основных примеров дизъюнктов S.

Доказательство. Предположим, что S невыполнимо. Пусть Т – полное семантическое дерево для S. Тогда по теореме Эрбрана (вариант 1) существует конечное замкнутое семантическое дерево Т, соответствующее Т. Пусть S - множество всех основных приме­ров дизъюнктов, которые опровергаются во всех опровергающих узлах T. S конечно, так как в Т содержится конечное число опро­вергающих узлов. Так как S ложно в каждой интерпретации S, то S невыполнимо.

Предположим, что существует конечное невыполнимое множе­ство S основных примеров дизъюнктов в S. Так как каждая интер­претация I для S содержит интерпретацию I множества S и I опро­вергает S, то I должна также опровергать S. Однако S опровергается в каждой интерпретации I. Следовательно, S опровергается в каждой интерпретации I множества S Поэтому S опровергается в каждой интерпретации множества S, значит, S невыполнимо.

Пример. Пусть S = {Р(х)Q(f(x), x), P(g(b)), Q(y, z)}. Это множество невыполнимо. Одно из невыполнимых множеств основных примеров дизъюнктов множества S есть S={ P(g(b))Q(g(b), b), P(g(b)) Q(f(g(b)), g(b))}.