Теормин 2014 (avasite), страница 2

Если формула ϕ общезначима, то существует успешный табличный вывод для таблицы Tϕ = <∅|ϕ>.

(следует из теоремы полноты табличного вывода)

Теорема Левенгейма-Сколема

Формула ϕ выполнима ⇐⇒ ϕ имеет модель с конечной или счетно-бесконечной предметной областью.

(Если ϕ выполнима, то тогда бы нашлась в соответствии с теоремой о полноте табличного вывода либо атомарная незакрытая таблица, либо счётная ветвь в табличном выводе)

Теорема Компактности Мальцева

Γ |= ϕ ⇐⇒ существует такое конечное подмножество Γ’, Γ’⊆ Γ, что Γ’|= ϕ.

(следствие означает соответствующую невыполнимость таблицы, т.е. наличие успешного табличного вывода, т.е. его конечность, т.е. количество формул к которым был применён табличный вывод – конечно, а значит остальное можно обрезать и для нового конечного набора формул – этот табличный вывод останется верным)

Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.

Здесь должна быть лекция 6, но из-за лагов с кодировкой у меня ничего не вышло, так что сокращённый вариант – т.е. без формулировок

Общая схема метода резолюций

Резольвента

Пустой дизъюнкт □

Эквивалентность – это лишь оператор в формуле: ϕ≡ψ ⇔ (ϕ→ψ)&(ϕ→ψ)

Равносильные формулы – это формулы для которых верно |= ϕ≡ψ

Теорема о равносильной замене

|= ψ≡χ => |= ϕ[ψ] ≡ ϕ[ψ/χ]

(Доказывается индукцией по числу связок и кванторов в формуле ϕ)

Предварительная нормальная форма (ПНФ) – ϕ= Q₁x₁Q₂x₂…Q_nx_n M(x₁, x₂, …, x_n)

Квантовая приставка

Теорема о ПНФ

Для любой замкнутой формулы существует предварительная нормальная формула

(Переименование переменных, потом удаление импликации, потом продвижение отрицания вглубь, вынесение кванторов наружу, приведение к КНФ)

Сколемовская стандартная форма (ССФ) – ∀₁x₁∀₂x₂…∀_nx_n M(x₁, x₂, …, x_n) (без ∃)

Теорема о ССФ

Для любой замкнутой формулы существует такая сколемовская стандартная формула, что одна выполнима тогда и только тогда, когда выполнима другая

(через лемму об удалении кванторов существования)

Лемма об удалении кванторов существования

Сколемовский терм

Сколемовская константа

Сколемизация

Теорема

Сколемовская стандартная форма невыполнима тогда и только тогда, когда множество формул (все отдельные конъюнкции с кванторами ∀) не имеет модели

Литеры

Невыполнимая, противоречивая система дизъюнктов – система не имеющая ни одной модели, в которой бы выполнялись все дизъюнкты

Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации

Метод резолюций:

Проверка общезначимости формулы ϕ сводится к проверке противоречивости системы дизъюнктов Sϕ.

Этап 1. Сведение проблемы общезначимости к проблеме противоречивости: ϕ -> ϕ0 = ¬ϕ

Этап 2. Построение предваренной нормальной формы (ПНФ). ϕ0 -> ϕ1 = Q1x1Q2x2. . . Qnxn(D1&D2& . . . &DN)

Этап 3. Построение сколемовской стандартной формы (ССФ). ϕ1 -> ϕ2 = ∀xi1∀xi2. . . ∀xik(D1&D2& . . . &DN)

Этап 4. Построение системы дизъюнктов. ϕ2 -> Sϕ = {D1, D2, . . . , DN},

ϕ общезначимая ⇐⇒ система дизъюнктов Sϕ противоречива.

Эрбрановские интерпретации — это специальная разновидность интерпретаций, в основе которых лежат свободные алгебры.

Пусть задана некоторая сигнатура σ = <Const, Func, Pred>. Тогда эрбрановским универсумом σ называется множество термов Hσ , где i = 0 H0 ={Const , если Const ≠ ∅; {c}, если Const = ∅ (эрбрановская константа)}, i → i + 1 Hi +1 = Hi∪ {f^(k)(t1, . . . , tk): f^(k)∈ Func, t1, . . . , tk ∈ Hi}

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

Эрбрановская H-интерпретация I_H = <Hσ, Const_H(с верхн. подчёрк), Func_H(с верхн. подчёрк), Pred(с верхн. подчёрк)> сигнатуры σ = <Const , Func , Pred> состоит из

• стандартной предметной области — эрбрановского универсума Hσ

• стандартной оценки констант: ConstH(c) = c, т. е. значением каждого константного символа c является его собственное изображение

• стандартной оценки функциональных символов: FuncH(f(n)) = f : f (t1, t2, . . . , tn) = f⁽ⁿ⁾(t1, t2, . . . , tn),т. е. каждый функциональный символ f играет рольконструктора термов эрбрановского универсума

• произвольной оценки предикатных символов.

Теорема о H -интерпретациях

Система дизъюнктов S выполнима тогда и только тогда, когда S имеет эрбрановскую модель, т.е. выполнима хотя бы в одной H -интерпретации.

(В одну сторону очевидно, а в другую – построим гомоморфное отображение)

Следствие

Система дизъюнктов S противоречива тогда и только тогда, когда S невыполнима ни в одной эрбрановской интерпретации.

Пусть P^(m) ∈ Pred, и t1, . . . ,tm ∈ Hσ — набор основных термов. Тогда формула P^(m)(t1, . . . , tm) называется основным атомом. Множество всех основных атомов называется эрбрановским базисом и обозначается B_H. Всякая H-интерпретация I задается подмножеством B^I истинных основных атомов: B^I= {P^(m)(t1, . . . ,tm) : I |= P^(m)(t1, . . . ,tm), {t1, . . . , tm} ⊆ H}.

Пусть имеется дизъюнкт D = ∀x1…∀xm (L1 ∨…∨ Lk) и набор основных термов t1, . . . , tm из эрбрановского универсума Hσ. Тогда дизъюнкт D’ = (L1 ∨ · · · ∨ Lk){x1/t1, . . . , xm/tm}, полученный из D подстановкой основных термов t1, …,tm вместо всех переменных дизъюнкта D называется основным примером дизъюнкта D.

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

Система дизъюнктов S = {D1, . . . , DN} противоречива ⇐⇒ существует конечное противоречивое множество G’ основных примеров дизъюнктов системы S.

(система противоречива <=> для каждой H-интерпретации она противоречива, т.е. любой основной пример для некоторого дизьюнкта – ложен, а дальше - опираясь на теорему Компактности Мальцева, т.е. что всегда можно выделить конечное подмножество из множества)

Правило вывода, разрешающее противоречия, называется правилом резолюции. Это правило можно применять до тех пор, пока не возникнет неустранимое противоречие D₁=L и D₂=¬L. Это и будет служить признаком противоречивости системы S.

Приведение выражений к общему виду называется унификацией.

Подстановка — это отображение θ: Var → Term.

Конечная подстановка θ = {x1/t1, x2/t2, . . . , xn/tn}. Eθ — применение подстановки θ к выражению E.

Пусть θ, η ∈ Subst. Композиция подстановок θη — это подстановка µ, которая определяется следующим соотношением: µ(x) = (xθ)η для любой x ∈ Var.

Утверждение

Пусть θ = {x1/t1, …, xn/tn}, η = {y1/s1, …, ym/sm}. Тогда подстановка µ = {x1/t1η, …, xn/tnη}∪ ({yi/si: yi∉{x1, x2, …, xn}} − {xj/tjη: xj = tjη} ), является композицией θη.

(Возьмём некоторую переменную z и рассмотрим все возможные случаи)

Пусть E1 и E2 — два логических выражения (термы, атомы, формулы и др.) Подстановка θ называется унификатором выражений E1 и E2, если E1θ = E2θ. Подстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2, если

1. θ — унификатор выражений E1 и E2

2. для любого унификатора η выражений E1 и E2 существует такая подстановка ρ, для которой верно равенство η = θρ

НОУ(E1, E2) — множество наиболее общих унификаторов выражений E1 и E2.

Задача унификации состоит в том, чтобы для двух выражений E1 и E2 выяснить, являются ли эти выражения унифицируемыми, и, в случае их унифицируемости, вычислить наиболее общий унификатор.

Лекция 8. Алгоритм Унификации.

Лемма (о связке)

Пусть x ∈ Var , t ∈ Term. Тогда

1. Если x ∉ Var_t, то {x /t} ∈ НОУ(x , t)

2. Если x ∈ Var_t и x ≠ t , то НОУ(x , t) = ∅.

(В первом случае проведём рассуждения для любой взятой переменной, а во втором – для любой подстановки длинна терма не сходится)

Подстановка θ называется унификатором системы уравнений E E: {t1 = s1; t2 = s2; …tn = sn} если для любого i , 1 ≤ i ≤ n, термы tiθ и siθ одинаковы. (Фактически, унификатор θ = {x1/r1, …, xk/rk} — это решение системы уравнений E в свободной алгебре термов)

Соответствующим образом определяется и наиболее общий унификатор системы уравнений

Cистема уравнений E называется приведенной, если E: {x1 = s1; x2 = s2; …; xn = sn} и при этом

1. {x1, . . . , xn} ⊆ Var

2. все переменные x1, ..., xn попарно различные

3. {x1, . . . , xn} ∩ = ∅.

Лемма (о приведенной системе)

Если система уравнений E. E: {x1 = s1; x2 = s2; …; xn = sn} является приведенной, то подстановка {x1/s1, x2/s2, …, xn/sn} является наиболее общим унификатором системы E.

(по лемме о связке)

Системы уравнений E1 и E2 называются равносильными, если НОУ(E1) = НОУ(E2).

Описание алгоритма унификации (Алгоритм Мартелли–Монтанари).

Это — недетерминированный алгоритм, состоящий из 6 правил, которые можно применять в любом порядке до тех пор, пока

1. либо ни одно из правил применить невозможно (построена приведенная система уравнений)

2. либо применяется правило, устанавливающее невозможность унификации.

Исходная система E0; i = 0;

while применимо одно из 6 правил do

выбрать правило R , применимое к Ei;

Ei ++ = R (Ei)

od

Правила преобразования решения уравнений.

1. уравнение f (t₁’, t₂’, …, t_k’) = f (s₁’, s₂’, …, s_k’) замещается совокупностью уравнений t₁’= s₁’, t₂’= s₂’, …, t_k’= s_k’

2. если в системе есть уравнение f(t₁’, …, t_k’) = g(s₁’, …, s_m’), где f, g ∈ Func ∪ Const , f ≠ g, то система уравнений не имеет решений: СТОП: “Нет унификатора"

3. уравнение s = x, где x ∈ Var, s ∉ Var , замещается уравнением x = s

4. уравнение s = s удаляется из системы

5. если в системе есть уравнение x = s , причем

   • x ∈ Var

   • x ∉ Var_s, и

   • переменная x встречается в каких-либо других уравнениях системы,

то ко всем другим уравнениям системы применяется подстановка {x/s}

1. если в системе есть уравнение x = s , причем x ≠ s , x ∈ Var_s, то система уравнений не имеет решений: СТОП: “Нет унификатора".

Теорема (об унификации)

Какова бы ни была система уравнений E.

1. алгоритм унификации Мартелли-Монтанари всегда завершает работу

2. если система уравнений E унифицируема, то в результате работы алгоритма унификации будет построена приведенная система уравнений, равносильная исходной системе E

3. если система уравнений E неунифицируема, то в результате работы алгоритма унификации будет выдано сообщение СТОП: НЕТ УНИФИКАТОРА.

(каждой системе уравнений сопоставляется тройка - <общее число неприведённых переменных, общее число функциональных символов, общее число уравнений>, а теперь разберём все 6 правил алгоритма и докажем, что в 4-х из них, где нет СТОП – характеристика убывает, а делать это бесконечно нельзя, в силу вспомогательной леммы. Так же не забываем доказать корректность – т.е. что после каждого правила система – эквивалентна (упоминая лемму о связке доказываем, что унификатор одной системы является унификатором и другой). + не забываем упомянуть про полноту)

Вспомогательная лемма.

В множестве троек натуральных чисел не существует бесконечно убывающей последовательности <k1, m1, n1> >>> ­<k2, m2, n2> ­>>> … >>> ­ <ki, mi, ni> ­>>> <k_{i +1}, m_{i +1}, n_{i +1}> >>> ­ …

Лекция 9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.

Пусть задано выражение E и подстановка θ. Подстановка θ: Var → Var называется переименованием, если θ — биекция. Выражение Eθ называется примером выражения E. Если Var_Eθ = ∅, то пример Eθ называется основным примером выражения E. Если θ — переименование, то пример Eθ называется вариантом выражения E.

Правило резолюции