АкушерствоАнатомияАнестезиологияВакцинопрофилактикаВалеологияВетеринарияГигиенаЗаболеванияИммунологияКардиологияНеврологияНефрологияОнкологияОториноларингологияОфтальмологияПаразитологияПедиатрияПервая помощьПсихиатрияПульмонологияРеанимацияРевматологияСтоматологияТерапияТоксикологияТравматологияУрологияФармакологияФармацевтикаФизиотерапияФтизиатрияХирургияЭндокринологияЭпидемиология

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

Определение. Пусть D – дизъюнкт из множества дизъюнктов S. Основным примером дизъюнкта D называется дизъюнкт, полученный из D заменой переменных на элементы эрбрановского универсума Н_¥.

Определение. Пусть B – эрбрановский базис множества дизъюнктов S. Семантическое дерево Т называется полным, если для любого элемента А базиса B множество I(p) содержит либо А, либо ØА.

Определение. Вершина v семантического дерева называется опровергающей, если I(v) опровергает основной пример некоторого дизъюнкта S. Вершина v называется максимальной опровергающей, если вершина v′, предшествующая v, опровергающей не является.

Определение. Вершина v семантического дерева называется выводящей, если все непосредственно следующие за ней вершины являются максимальными опровергающими.

Пусть S={P(x), ØP(x)ÚQ(f(y)), ØQ(f(a))} множество дизъюнктов примера 1 предыдущего параграфа. Дерево, изображенное на рис.4.7, является семантическим деревом для S. Вершина v этого дерева является выводящей вершиной, а никакие другие вершины выводящими не являются.

Рис. 4.7

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

Следующее утверждение – знаменитая теорема математической логики, которая является основой многих алгоритмов доказательства теорем. Она называется теоремой Эрбрана.

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

Доказательство теоремы 4.6 использует известное математике утверждение, которое называется леммой Кенига. Сформулируем ее.

Лемма. Если Т – бесконечное дерево, из каждого узла которого выходит конечное число дуг. Тогда дерево Т содержит бесконечный p путь, начинающийся от корня.

Доказательство леммы Кенига приводить не будем. С ним можно познакомиться по книге С.Клини, указанной в списке литературы.

Приведем доказательство теоремы 4.6. Докажем вначале необходимость. Пусть множество дизъюнктов S невыполнимо и Т – полное семантическое дерево для S. Рассмотрим максимальный путь p в дереве Т. По определению полного семантического дерева для каждой атомарной формулы А эрбрановского базиса B, либо А, либо ØА принадлежит I(p). Это означает, что I(p) есть H-интерпретация множества S. Поскольку S невыполнимо, то I(p) опровергает основной пример D′ некоторого дизъюнкта D из S. Дизъюнкт D′ конечен, поэтому путь p должен проходить через максимальную опровергающую вершину дерева Т. В каждом максимальном пути отметим такую вершину. Пусть Т – корневое поддерево дерева Т, листьями которого являются отмеченные вершины. В силу леммы Кенига. Т′ – конечное поддерево дерева Т. Дерево T′ по построению является замкнутым. Необходимость доказана.

Докажем достаточность. Пусть полное семантическое дерево Т содержит конечное замкнутое поддерево T′. По определению поддерева (см.начало данного параграфа) отсюда следует, что каждый максимальный путь дерева Т содержит опровергающую вершину. Множество всех максимальных путей полного семантического дерева исчерпывает все H-интерпретации множества S. Следовательно S ложно при всех H-интерпретациях. По теореме 4.5 S невыполнимо

Дата добавления: 2015-09-27 | Просмотры: 807 | Нарушение авторских прав