yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->5.4. Эрбрановский универсум множества дизъюнктов.

Математическая логика

5.4. Эрбрановский универсум множества дизъюнктов.

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

Определение 5.3. Пусть Н0 - множество констант, встречающихся в S. Если никакая константа не встречается в S, то Н0 состоит из одной константы, скажем Н0 =(а). Для i=1,2,... пусть Hi+1 есть объединение H1 и множества всех термов вида fn(t1,...,tn) (при всех n) для всех функций fn, встречающихся в S, где tj (j=l,...,n) принадлежит Hj. Тогда каждое H1 называется множеством констант 1-го уровня для S и Н. называется эрбрановским универсумом S.

Пример. Пусть S=(P(a), ¬P(x)vP(f(x))}. Тогда

H0={a}

H1={a, f(a) }

H2={а}, f(a), f(f(a))}

…………………………..

H={a, f(a), f(f(a)), f(f(f(a))),… }

Пример. Пусть S={P(x)vQ(x),R(z),T(y)v¬W(y) }. Так как не существует никаких констант в S, положим Н0={а}. Поскольку не существует никаких функциональных символов в S, следовательно Н=Н01=...={а}

Определение 5.4. Пусть S есть множество дизъюнктов. Тогда множество основных атомов вида Рn (t1,...,tn) для всех n-местных предикатов Рn, встречающихся в S, где t1,...,tn - элементы эрбрановского универсума S, называется множеством атомов множества S или эрбрановским базисом S3.

Определение 5.5. Основной пример дизъюнкта С множества дизъюнктов дизъюнкт,    полученный    заменой    переменных    в    С    на    члены всякого универсума S.

Пример. Пусть S={P(x), Q(t(y))vR(y)}. С=P(х) - дизъюнкт в S и Н={а, f(a),...} - эрбрановский универсум S. Тогда Р(а) и P(f(f(a))) есть основные примеры С.

Определение 5.6. Пусть S - множество дизъюнктов, Н - эрбрановский универсум   S   и   1   -   интерпретация   S   над   Н.   Говорят,   что   I   есть   Н- интерпретация множества S, если она удовлетворяет следующим условиям: 1. отображает все константы из S в самих себя.         2. Пусть f есть n-местный функциональный символ и h1,...,hn – элементы H. B I через f обозначается функция, которая отображает (h1....,hn) (элемент из Hn) в  f(h1,...,hn) ( элемент из Н).

При   этом  не  возникает  никаких  ограничений  при  придании  значения любому n-местному предикатному символу в S. Пусть А={А1, А2,… Аn, ...} – эрбановский базис множества S. Н-интерпретацию I удобно представлять в виде l={m1,m2, .... mn, ...}, где m, есть или Аj или ¬Aj для j=l,2,... Смысл этого множества в том, что если mj есть Aj, то атому  Аj присвоено значение «истинно», в противном случае - значение "ложно".

Пример.   Рассмотрим   множество   S={P(x)vQ(x), R(f (у))}.   Эрбрановский универсум Н для S есть Н={а, f(a), f(f(a)), ...}. В S входят три предикатных символа: Р, Q и R. Следовательно, эрбрановский базис S есть

А={Р(а), Q(a), R(a), P(f(a)),Q(f(a)), R(f(a)), …}.

Некоторые Н интерпретации множества S суть

I1={Р(а), Q(a), R(a), Р(f(a)), Q(f(a)), Rf(a)),… },

I2={¬P(a), ¬Q(a), ¬R(a), ¬P(f(a)), ¬Q(f(a)), ¬R(f(a))… }

I3={P(a),Q(a), ¬R(a), P(f(a)),Q(f(a)), ¬R(f(a))… }

Теорема 5. 3. Множество дизъюнктов S невыполнимо тогда и только тогда, когда S ложно при всех Н-интерпритациях в S.

Доказательство. Первая половина теоремы очевидна, так как по определению S невыполнимо тогда и только тогда, когда S ложно при всех интерпретациях на этой области.

Чтобы доказать вторую половину теоремы, предположим, что S ложно при всех Н-интерпретациях в S. Положим, что S выполнимо. Тогда существует такая интерпретация I на некоторой области D, Что S истинно при I. Пусть I* есть Н- интерпретация, соответствующая I. Тогда S истинно при I*. Это противоречит предположению, что S ложно при всех Н-интерпретациях в S. Следовательно, S должно быть невыполнимо, что и требовалось доказать.

Таким образом мы достигли цели, установленной в начале этого параграфа, т. е. нам необходимо рассматривать Только интерпретации над эрбрановским  универсумом   (или,  более   строго,   -   Н- интерпретации   для проверки того, выполнимо множество дизъюнктов или нет. Поэтому впредь, упоминая интерпретацию, мы будем иметь в виду Н-интерпретацию.

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

Определение 5.7. Если А - атом, то говорят, что две литеры А и ¬А  контрарны друг другу, и множество {А, ¬А} называется контрарной парой. Отметим, что дизъюнкт есть тавтология, если он содержит контрарную пару.

Определение 5.8. Пусть S - множества дизъюнктов и  А - его эрбрановский базис. Семантическое дерево для S есть растущее вниз дерево Т, в которой каждому ребру приписано конечное множество атомов или отрицаний атомов из А таким образом, что:

(i) Из каждого узла N выходит только конечное число ребер L1,…, Ln. Пусть Q1 - конъюнкция всех литер, приписанных к Li i=l,…,n. Тогда Q1vQ2v...vQn - общезначимая пропозициональная формула.

(ii) Пусть для каждого узла N I(N) есть объединение всех множеств, приписанных ребрам ветви, ведущей к N. Тогда I(N) не содержит контрарных пар.

Определение 5.9. Пусть A= {A1, A2, ..., Аn, ...} - эрбрановский базис множества S. Говорят, что семантическое дерево для S будет полным тогда и только тогда, когда для каждого i (i=1,2,...) и каждого конечного узла N семантического дерева (т. е. для узла, из которого не выходит никаких ребер) I(N) содержит либо A либо ¬A1.

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

Определение 5.10. Узел N называется опровергающим, если I(N) опровергает некоторый основной пример дизъюнкта в S, но для любого предшествующего N узла N' I(N') не опровергает никакого основного примера дизъюнкта в S.

Определение 5.11. Говорят, что семантическое дерево Т будет закрытым, тогда и только тогда, когда каждая ветвь Т оканчивается опровергающим узлом.

Пример. Пусть S={P, QvR, ¬Pv ¬Q, ¬Pv ¬R}.

Эрбрановский базис множества S есть A=(P,Q,R). Тогда опровергающими примерами будет множество {Р, QvR, pvQ, PvR}.

Пример. Рассмотрим S={P(x), ¬P(x)vQ(f(x)), ¬Q(f(a))}. Эрбрановский базис множества S есть А = {Р(а), Q(a), P(f(a)), Q(f(a), ... }. Опровергающими примерами будут: {Р(а), P(a)vQ(f(a)), Q(f(a)) }.

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

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

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

Доказательство:   Допустим,   что   S   невыполнимо.   Пусть   Т   -   полное "   семантическое дерево для S. Для каждой  ветви В дерева  Т пусть  I`B -множество  всех литер,  приписанных  всем  ребрам  ветви   В,  Тогда   IВ есть интерпретация для S. Так как S невыполнимо,  то  IВ должна  опровергать основной пример С` дизъюнкта С в S. Однако так как С' конечно, то на В должен   существовать   опровергающий   узел   NB   (лежащий   на    конечном расстоянии от корня).  Поскольку  каждая  ветвь Т  имеет опровергающий узел, То существует замкнутое Семантическое дерево Т' для S. Далее, так как из  каждого узла  в Т' выходит только  конечное  число ребер,   то Т' должно быть конечным (т. е. число узлов б Т' конечно), иначе мы могли бы найти   бесконечную   ветвь,   не содержащую   опровергающих   узлов.   Таким образом; мы заканчиваем доказательство первой половины 'теоремы.

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

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

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

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

Поэтому S опровергается а каждой интерпретации множества S' значит, S невыполнимо.

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

 

34