Сводка определений - 1 (Старые варианты экзамена), страница 2

Для любой замкнутой формулы ϕ существует равносильная предвареннаянормальная формула ψ.Сколемовская стандартная форма (ССФ) — предваренная нормальная форма, у которой в кванторной приставке отсутствуют кванторы существования: φ =Теорема о ПНФ∀xi1 ∀xi2 . . . ∀xim M (xi1 , xi2 .

. . xim ). Для любой замкнутой формулы ϕ существует такая сколемовская стандартная форма ψ, что ϕ выполнима ⇔ ψ выполнима.Леммаобудалениикванторовсуществования.Пусть φ=∀x1 ∀x2 . . . ∀xk ∃xk+1 ϕ0 (x1 , x2 . . . xk+1 ) — замкнутая формула, k > 0, и k-местный функциональный символ f (k) не содержится в формуле ϕ. Тогда формула ϕ выполнима тогда и толькотогда, когда выполнима формула ψ = ∀x1∀x2 . . . ∀xk ϕ0(x1, x2 . . .

xk , f (k)(x1, x2, . . . , xk ))Сколемизация — процесс удаления кванторов ∃Сколемовский терм — терм f (k) (x1 , . . . , xn ), который подставляется вместо удаляемой переменной xk+1, связанной квантором существования ∃.Если k = 0, то терм называется сколемовской константой.Теорема о невыполнимости сколемовской формулы. Сколемовская стандартная форма ϕ = ∀x1∀x2 .

. . ∀xm(D1 ∧ D2 ∧ · · · ∧ DN ) невыполнима тогда и только тогда, когда множествоформул Sϕ = {∀x1∀x2 . . . ∀xmD1, ∀x1∀x2 . . . ∀xmD2, . . . , ∀x1∀x2 . . . ∀xmDN } не имеет модели.Дизъюнкт — формула из множества Sϕ . Дизъюнкт имеет вид ∀x1 ∀x2 . . . ∀xm (L1 ∨ L2 ∨ · · · ∨Lk ), где Li — литера, которая является либо атомом, либо отрицанием атома.Пустой дизъюнкт — дизъюнкт, не имеющий литер и тождественно ложный.Невыполнимая (противоречивая) система дизъюнктов — система дизъюнктов, неимеющая модели.Теорема о противоречивости системы дизъюнктов. Система дизъюнктов S ={D1 , D2 , .

. . , Dn } протеворечива тогда и только тогда, когда для каждой интерпретации I в системе S найдется такой дизъюнкт Di = ∀x1∀x2 . . . ∀xm(L1i ∨ L2i ∨ · · · ∨ Lk i), а в предметной областитакой набор d1, . . . , dn, для которых имеют место: I 2 L1i[d1, . . . , dn] . . . I 2 Lk i[d1, .

. . , dn]Эрбрановские интерпретации (H-интерпретации) — это специальная разновидность интерпретаций, в основе которых лежат свободные алгебры.Теорема о ССФii5Эрбрановский универсумтаций.(H-универсум) — предметная область эрбрановских интерпре-Эрбрановским универсумом Hσмножество Hσ =∞Si=0Hi ,где(Const• i = 0 H0 ={c}для сигнатуры σ =< Const, F unc, P red > называетсяесли Const 6= ∅если Const = ∅(эрбрановская константа)• i → i + 1 Hi+1 = Hi ∪ {f (k) (t1 , t2 , . .

. , tk ) : t(k) ∈ F unc , t1 , t2 , . . . , tk ∈ Hi }— терм эрбрановского универсума. Не содержат переменных.Эрбрановская интерпретация IH =< Hσ , ConstH , F uncH , P red > сигнатурыConst, F unc, P red > состоит изОсновной терм••••σ =<стандартной предметной области — эрбрановского универсума Hσстандартной оценки констант ConstH (c) = c, т.е.

значением каждого константного символаявляется его отображениестандартной оценки функциональных символов F uncH (f (n)) = f : f (t1, . . . , tn) =f (n) (t1 , . . . , tn ), то есть каждый функциональный символ f играет роль конструктора термов эрбрановского универсумапроизвольной оценки предикатных символовТеорема о H-интерпретациях. Система дизъюнктов S выполнима тогда и только тогда,когда имеет эрбрановскую модель, т.е.

выполнима хотя бы в одной H-интерпретации.Основной атом — формула P (m) (t1 , . . . , tm ), где P (m) ∈ P red , t1 , . . . , tm ∈ Hσ (набор основных термов)Эрбрановский базис (BH ) — набор всех основных атомов.Всякая H-интерпретация I задается подмножеством B I истинных основных атомов: B I ={P (m) (t1 , .

. . , tm ) : I |= P (m) (t1 , . . . , tm ), t1 , . . . , tm ∈ H}— дизъюнкт D0 = (L1 ∨L2 ∨ · · · ∨ Lk ){x1 /t1 , . . . , xm /tm }, полученный из D путем подстановки основных термов t1 , . . . , tm ∈Hσ эрбрановского универсума.Основной пример дизъюнкта D = ∀x1 ∀x2 . . . ∀xm (L1 ∨L2 ∨· · ·∨Lk )Теорема о противоречивости системы дизъюнктов (через эрбрановские интерпретации)S = {D1 , . . . , DN }⇔. Система дизъюнктовпротиворечивадля каждой H-интерпретации в S найдется такой дизъюнкт D = (L1i ∨ L2i ∨ · · · ∨ Lk i) и такойнабор основных термов t1, . .

. , tm, для которых имеет место I 2 (L1i ∨ L2i ∨ · · · ∨ Lk i)[t1, . . . , tm]ii⇔для каждой H-интерпретации существует основной пример D0 = Di{x1/t1, . . . , xm/tm} дизъюнктаD ∈ S , для которого I 2 D0Теорема Эрбрана. Система дизъюнктов S = {D1 , . . . , DN } противоречива тогда и толькотогда, когда существует конечное противоречивое множество G0 основных примеров дизъюнктовS.6. Система дизъюнктов S противоречива тогда и только тогда,когда S невыполнима ни в одной эрбрановской интерпретации.Композиция подстановок µ = θη , θ, η ∈ Subst, которая определяется как µ(x) = (xθ)ηдля любой x ∈ V ar.Утверждение.

Пусть θ = {x1/t1, . . . , xn/tn} , η = {y1/s1, . . . , ym/sm}, тогда подстановка µ ={x1 /t1 η, . . . , xn /tn η} ∪ {yi /si : yi ∈/ {x1 , . . . , xn }} − {xj /tj η : xj = tj η}.Унификатор — подстановка θ логических выражений E1 , E2 такая, что E1 θ = E2 θ .Наиболее общий унификатор (НОУ) — унификатор выражений E1 , E2 такой, что длялюбого унификатора η для этих же выражений существует подстановка p такая, что η = θpявляется композицией θ и p.Задача унификации — для двух выражений E1 , E2 выяснить, являются ли они унифицируемыми и, в случае унифицируемости, вычислить наиболее общий унификатор.Лемма о связке. Пусть x ∈ V ar, t ∈ T erm, тогдаСледствие теоремы Эрбрана1) если x ∈/ V art, то {x/t} ∈ НОУ(x, t)2) если x ∈ V art , x 6= t, то НОУ(x, t) = ∅Приведенная система— система уравненийx1 = s 1x = s22E=...xn = s nи при этом• x1 , .

. . , xn ⊆ V ar•все переменные x1, . . . , xn попарно различны• {x1 , . . . , xn } ∩nSV arsi = ∅i=1. Если система E является приведенной, то унификатор{x1 /s1 , . . . , xn /sn } является ее наиболее общим унификатором.Равносильные системы E1 , E2 — такие системы, что НОУ(E1 ) = НОУ(E2 )Алгоритм унификации (алгоритм Мартелли-Монтанари) — недетерменированныйалгоритм из 6 правил, которые можно применять в любом порядке до тех пор, пока ни одно изправил нельзя применить или не применялось одно из правил, устанавливающих невозможностьунификации.Теорема об унификации. Какова бы ни была система уравнений EЛемма о приведенной системе1) Алгоритм Мартелли-Монтари всегда завершает свою работу2) Если система Е унифицируема, то в результате работы алгоритма будет построена приведенная система, равносильная Е.3) Если система Е неунифицируема, то в результате работы алгоритма применено правило,устанавливающее невозможность унификации.7Переименованиежением.— подстановка θ : V ar → V ar такая, что θ является биективным отобра-Е — выражение EθОсновной пример — пример такой, что V arEθ = ∅.Вариант выражения — выражение Eθ , если θ является переименованием.Пустая (тождественная) подстановка — переименование.D ,DПравило резолюции.

(D ∨D )θ , где:Пример выражения011202• D1 = D10 ∨ L1 , D2 = D20 ∨ ¬L2• θ = НОУ(L1 , L2 )— два дизъюнкта— дизъюнкт D0 = (D10 ∨ D20 )θКонтрактная пара — пара литер L1 и ¬L2, где:Правило склейки. (D D∨L )θРезольвента дизъюнктов D1 , D201• D1 = D10 ∨ L1 ∨ L2• θ = НОУ(L1 , L2 )11— дизъюнкт— дизъюнкт D0 = (D10 ∨ L1)θСклеиваемая пара — пара литер L1 и L2Склейка дизъюнкта D1Резолютивный вывод системы дизъюнктов S = {D1 , .

. . , DN } — конечная последовательность дизъюнктов D10 , D20 , . . . , Dn0 (резолютивно выводимые дизъюнкты) такая, что для любогоi, 1 6 i 6 n выполняется одно из трех условий:1) либо Di0 — вариант некоторого из дизъюнктов из S2) либо Di0 — резольвента дизъюнктов Dk0 , Dj0 , k, j < i3) либо Di0 — склейка дизъюнктов Dj0 , j < iУспешный резолютивный вывод (резолютивное опровержение) — резолютивный вывод,который оканчивается пустым дизъюнктом 2.Теорема корректности резолютивного вывода. Если из системы дизъюнктов S резолютивно выводим пустой дизъюнкт 2, то S — противоречивая система дизъюнктов.Теорема о полноте резолютивного вывода.

Если S — противоречивая система дизъюнктов, то из S резолютивно выводим пустой дизъюнкт 2.Метод резолюций: корректен, полон, алгоритмизируем.Полная стратегия резолютивного вывода — такая стратегия, которая позволяет вывести пустой дизъюнкт 2 из любой противоречивой системы дизъюнктов.Семантическая резолюция (11.5)8. Если система дизъюнктов S противоречива, то для любойинтерпретации I существует успешный I-резолютивный вывод пустого дизъюнктов 2 из S.Линейная резолюция (11.8)Теорема полноты линейного резолютивного вывода. Если система дизъюнктов S противоречива, а система дизъюнктов S\{D0} непротиворечива, то существует успешный линейныйрезолютивный вывод пустого дизъюнкта 2 из S.Теорема полноты I-резолюции9.