ЛМвИИ (1086253), страница 11
Текст из файла (страница 11)
Более того, достаточно зафиксировать одно такое множество H для данногомножества дизъюнктов S (кратко H(S)), что S невыполнимо тогда и только тогда, когда S ложнопри всех интерпретациях на этом множестве. Такое множество H(S) называют универсумомЭрбрана для S и определяют следующим образом:1. Множество всех констант из S принадлежит или, если в H(S) нет констант,принимается, что H(S) принадлежит некая произвольная константа а.2.
Если термы принадлежат H(S), то H(S) принадлежит также f(t1, …, tn), гдеf-функциональный символ, упомянутый в S.Примеры.1. Пусть S={P(x), R(x, y), Q(y)}, тогда H(S) ={a}.2. Пусть S={P(a), R(x, y), Q(y)}, тогда H(S) ={a}.3. Пусть S={P(a), R(x, b), Q(c)}, тогда H(S) ={a,b,c}.4. Пусть S={P(a), R(f(x), b), Q(φ(x, z))},ToгдaH(S)={a, b, f(a), f(b), φ(a, a), φ(a, b), …, f(f(a)), …, f(φ(a, b)), …, φ(f(φ(a, a)), φ(f(a), φ(b, a))), …}.Наличие хотя бы одной функции делает универсум Эрбрана бесконечным (счетным).Вне зависимости от интерпретации никаких Термов для S, выходящих за рамкиуниверсума Эрбрана, быть не может.Фундаментальной (основной) конкретизацией (Прим.: В некоторых источниках [35]термин instance в русском переводе дан в значении пример.
Более точным по смыслу, на нашвзгляд, является значение конкретизация.) дизъюнкта С называется дизъюнкт, полученныйзамещением переменных в С членами универсума Эрбрана H(S) таким образом, что всевхождения одной и той же переменной в С заменяется на один и тот же терм. Аналогичноопределяется фундаментальный пример предиката.Базой Эрбрана для всех множеств дизъюнктов S называется множество всехфундаментальных конкретизации предикатов из S.Интерпретация I называется H-интерпретацией (интерпретацией Эрбрана) тогда итолько тогда, когда она удовлетворяет следующим условиям:1. I отображает все константы из S в себя.2.
Пусть f есть n-местный функциональный символ и t1, …, tn - элементы H(S), тогда.I: (t1, …, tn) → f(t1, …, tn), т.е. I отображает кортеж термов в соответствующее значениефункции f. H-интерпретация относится только к термам и не накладывает никакихограничений на предикаты (атомы).Пусть А = {А1, …, An , ...} является базой Эрбрана для S.
Тогда H-интерпретация можетбыть представлена множеством I{m1, …, mn , ...}, где mj есть Aj или ¬Аj. При этом, если mj естьAj, то Aj приписывается значение "истинно", иначе Aj приписывается значение "ложно".Существует теория, утверждающая, что множество дизъюнктов невыполнимо тогда и толькотогда, когда S ложно при всех H-интерпретациях.Таким образом, мы ограничили исходное множество универсумом Эрбрана, амножество интерпретаций H-интерпретацией.Примеры.1.
Множество дизъюнктов S = {R(x), P(g(y)) v Q(y)}, универсум Эрбрана H(S) = {a, g(a),g(g(a)), ...}, база Эрбрана A = {R(a), P(a), Q(a), R(g(a)), P(g(a)), Q(g(a)), ...}, примерH-интерпретаций:I1 = {R(a), P(a), R(g(a)), P(g(a)), Q(g(a)), ...},I2 = {¬R(a), ¬P(a), ¬Q(a), ¬R(g(a)), ¬P(g(a)), ¬Q(g(a)), ...},I3 = {R{a), ¬P(a), Q(a), R(g(a)), ¬P(g(a)), Q(g(a)), ...}.2. S = {Q(x)v¬R(x), P(x), Q(b)}, H(S) = {b}, A = {Q(b), R(b), P{b)}.I1 = {Q(b), R(b), P(b)},I2 = {Q(b), R(b), ¬P(b)},I3 = {Q(b), ¬R(b), P(b)},…...................................I8 = {¬Q(b), ¬R(b), ¬P(b)}.Здесь множество S истинно на I1 и I3 и ложно на всех остальных интерпретациях.3.
S = {P(x), ¬P(x)}, H(S) = {a}, A = {P(a)}.I1 = {P(a)},I2 = {¬Р(а)}.Здесь множество S невыполнимо, так как оно ложно как в I1, так и в I2.Заметим, что эрбрановская интерпретация (и зрбраиовская модель) - этоинтерпретация (и соответственно модель), у которой область интерпретации включаетмножество (предполагаемое непустым) конкретных термов рассматриваемого языка, причемлюбому конкретному терму сопоставляется он сам. Эрбрановская модель полностьюхарактеризуется множеством конкретных атомов, истинных в рассматриваемой модели.Следовательно, эрбрановскую модель можно отождествлять с упомянутым множеством исравнивать модели между собой, пользуясь теоретико-множественным отношением включения.Семантическое дерево - это дерево, в котором каждый путь от корня к листусоответствует отдельной H-интерпретации. Пусть, например, S = {Q(x)vR(y), P(x)}, тогдаA={Q(a), R(a), P(a)}.
Семантическое дерево для данной базы Эрбрана представлено на рис.2.1.Например, в листе 7 заканчивается путь, соответствующий Н-интерпретации I7 = {¬P(a), ¬Q(a),R(a)}. Кстати, данная интерпретация не удовлетворяет S. так как атом ¬Р(а) не удовлетворяетсостоящему из одного предиката дизъюнкту Р(х).Вершины, в которых впервые была установлена неудовлетворительностьинтерпретации, называются неблагоприятными. Семантическое дерево, опирающееся толькона неблагоприятные вершины, называется замкнутым.
Вершина замкнутого дерева,соединенная ребрами только с неблагоприятными вершинами, называется вершиной вывода.Рис. 2.1. Семантическое деревоПримеры.1. Пусть S = {P(x), Q(a)vR(y), ¬P(x)v¬Q(x), P(x)v¬R(a)}, тогда H(S) = {a},A = {P(a), Q(a), R(a)}.Рассмотрим все возможные интерпретации I1, …, I8, можно убедиться, что ни одна неудовлетворяется (рис. 2.2).Рис. 2.2. Замкнутое деревоРис. 2.3.
Замкнутое дерево2. Пусть S = {R(x), ¬R(x)vQ(f(x)), ¬Q(f(x)), тогда A = {R(a), Q(f(a)), Q(a), R(f(a)),Q(f(f(a))), R(f(f(a))), ...}. В вершине 3 невыполним дизъюнкт R(x), а в вершине 5 дизъюнкт¬R(x)vQ(f(x)), в вершице 4 — дизъюнкт ¬Q(f(x)) (рис. 2.3.).Теорема Эрбрана. Множество дизъюнктов S невыполнимо тогда и только тогда,когда любому полному семантическому дереву для S соответствует конечное замкнутоедерево.Доказательство. Допустим, что невыполнимо, тогда множество атомов, приписанныхребрам соответствующей ветви, опровергает фундаментальный дизъюнкт С из S.
Так как любойфундаментальный пример дизъюнкта конечен, то на ветви конечной длины существуетнеблагоприятная вершина. Поскольку каждая ветвь имеет неблагоприятную вершину, то для Sсуществует замкнутое дерево. Но из каждой вершины выходит конечное число ребер,следовательно, замкнутое дерево конечно.Наоборот, если для каждого семантического дерева для S существует конечноезамкнутое дерево, то каждая его ветвь содержит неблагоприятную вершину, т.е.
каждаяинтерпретация опровергает S. Следовательно S невыполнимо.В литературе чаще встречается другая формулировка этой теоремы, которую приведембез доказательства.Теорема Эрбрана (второй вариант). Множество дизъюнктов невыполнимо тогда итолько тогда, когда существует конечное невыполнимое множество S' фундаментальныхконкретизацией дизъюнктов S.Важность теоремы Эрбрана состоит в том, что она гарантирует доказательствонепротиворечивости за конечное число шагов. И наоборот, существующее противоречие можетбыть всегда достигнуто за конечное число шагов, каковы бы ни были значения истинности,даваемые функциям, присутствующим в гипотезах и заключениях.2.5.1.
Применение теоремы Эрбрана. Метод Девиса иПатнема.Метод Девиса-Патнема основан на втором варианте теоремы Эрбрана. Для решениявопроса о невыполнимости конечной конъюнктивной нормальной формы S = G1^G2^...^Gnнеобходимо применить процедуру, состоящую из описанных ниже правил.
На каждом шагеконъюнкция S преобразуется в новую конъюнкцию S' такую, что S невыполнима, если и толькоесли невыполнима S'. Или порождается пара конъюнкций S' и S'' таких, что конъюнкция Sневыполнима, если и только если невыполнимы обе конъюнкции S' и S''. Процедура должназавершаться за конечное число шагов, так как число различных литералов, входящих в S, накаждом шаге сокращается.Метод составляют следующие правила:1. Правило однолитерных дизъюнктов.a) Если в S имеется пара однолитерных основных дизъюнкта Gj = l Gj = ¬l, то Sневыполнима.b) Если S содержит однолитерный дизъюнкт Gj = l, то S' получается удалением l из Sвсех дизъюнктов, содержащих (включающих Gj ) и затем удалением всехвхождений ¬l из оставшихся основных дизъюнктов. Если S' пусто, то S выполнима.2.
Правило чистых литер.Литера l в основном дизъюнкте из S называется чистой, если ¬l не встречается ни водном основном дизъюнкте. Если литера l чистая, то удаляются все основныедизъюнкты, содержащие l. Оставшаяся часть S' невыполнима, если невыполнима S.Если не остается дизъюнктов, то S выполнима.3. Правило расщепления.Если S можно представить в виде(A1vl)^...^(Amvl)^(B1v¬l)^...^(Bnv¬l)^R, где Ai, Вi и R свободна от l и ¬l, то получимконъюнкции S' = A1^...^Am^R и S'' = B1^...^Bn^R. S невыполнима, если и только если(S'vS'') невыполнима, т.е. S' и S'' невыполнимы.4. Правило тавтологии.Удаляются все тавтологичные основные дизъюнкты из S. Оставшаяся часть S'невыполнима тогда и только тогда, когда невыполнима S.Пример.
Пусть S = [P1(a)vP2(b)] ^ [P1(a)v¬P3(a)] ^ [¬P1(a)vР3(а)] ^ [¬Р1(а)v¬Р2(b)] ^[Р3(а)v¬Р2(b)] ^ [¬Р3(а)vР2(b)]С помощью построенного дерева можно проследить доказательство невыполнимости S.Следовательно, S невыполнима.Пример.Пусть S = [Р2(b)]^¬Р2(b)^[¬Р1(а)v¬Р2(b)v¬Р3(a)].Применив правило по ¬P2(b), получим[¬Pl(a)v¬P3(a)].Повторив правило 1b по Р1(а), получим¬P3(a).Наконец, применение еще раз правила 1b по Р3(a), приводит к удалению всехдизъюнктов из S. Следовательно, S выполнимо.2.6. Метод резолюции для логики предикатов первогопорядка.По существу метод (принцип) резолюции был обоснован Ж.Эрбраном в 1930г. Первымреализовал на ЭВМ идеи Эрбрана Дж.Робинсон в 1963г.Метод резолюции - один из методов доказательства от противного.
Основная идеяметода заключается в попытке вывести из множества дизъюнктов S пустой дизъюнкт, длякоторого нет интерпретаций и который тем самым гарантирует невыполнимость множествадизъюнктов. Процесс вывода пустого дизъюнкта может быть представлен процессом сведениячисла вершин замкнутого дерева к единственной неблагоприятной вершине.Для иллюстрации идеи вернемся, например, к замкнутому дереву на рис. 2.3. Здесьвершина вывода 2 не является неблагоприятной. Однако, если проанализировать вершины 4 и 5,в которых невыполнимы дизъюнкты ¬Q(f(x)) и ¬R(x)vQ(f(x)), соответственно, то можно сделатьвывод, что одновременная выполнимость этих двух дизъюнктов возможна только в случае, есливыполнен (истинен в данной модели) новый дизъюнкт.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
