8. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема Эрбрана (Лекции), страница 2

. . , tk ) = P(α(t1 ), . . . , α(tk ))Эрбрановские интерпретацииДоказательство. (⇒):Предположим, что IH не является моделью для SТогда существует дизъюнкт A1 ∨ · · · ∨ Am ∨ ¬B1 ∨ · · · ∨ ¬Bq ∈ S,такой что(Ai , Bj — атомы)IH 6|= ∀exn (A1 ∨ · · · ∨ Am ∨ ¬B1 ∨ · · · ∨ ¬Bq )Значит, существуют основные термы (предметы Hσ ) t1 , . . .

, tn ,такие чтоIH 6|= A1 [t1 , . . . , tn ], . . . , IH 6|= Am [t1 , . . . , tn ]IH |= B1 [t1 , . . . , tn ], . . . , IH |= Bq [t1 , . . . , tn ]Отображение α — гомоморфизм интерпретации IH винтерпретацию I:α(f(t1 , . . . , tk )) = f(α(t1 ), . . . , α(tk ))Значит, для любого атома A верно:IH |= A[t1 , . . . , tn ] ⇔ I |= A[α(t1 ), . . . , α(tn )]Эрбрановские интерпретацииДоказательство. (⇒):A1 ∨ · · · ∨ Am ∨ ¬B1 ∨ · · · ∨ ¬Bq ∈ SIH 6|= A1 [t1 , .

. . , tn ], . . . , IH 6|= Am [t1 , . . . , tn ]IH |= B1 [t1 , . . . , tn ], . . . , IH |= Bq [t1 , . . . , tn ]IH |= A[t1 , . . . , tn ] ⇔ I |= A[α(t1 ), . . . , α(tn )]ТогдаI 6|= A1 [α(t1 ), . . . , α(tn )], . . . , I 6|= Am [α(t1 ), . . . , α(tn )]I |= B1 [α(t1 ), . . . , α(tn )], . . . , I |= Bq [α(t1 ), . . . , α(tn )]иI 6|= ∀exn (A1 ∨ · · · ∨ Am ∨ ¬B1 ∨ · · · ∨ ¬Bq )Получено противоречие с тем, что I — модель для SЗначит, предположение о том, что интерпретация IH не являетсямоделью, неверноHЭрбрановские интерпретацииМожно ли удобно задавать H-интерпретации?BH — это эрбрановский базис: множество всех атомов,построенных над термами эрбрановского универсумаH-интерпретация I полностью определяется тем, какие атомыиз BH в ней истинны, то есть множествомB I = {A | A ∈ BH , I |= A}Например,IIIесли B I = ∅, то все основные атомы ложны в Iесли B I = BH , то все основные атомы истинны в Iмножество B I ∩ B J определяет интерпретацию, в которойистинны те и только те основные атомы, которые истинныв обеих интерпретациях I, JДалее эрбрановские интерпретации будем отождествлять сподмножествами эрбрановского базисаТеорема ЭрбранаЧто ещё полезного можно извлечь из H-интерпретаций?Система дизъюнктов S противоречива⇔Для каждой H-интерпретации I найдутся дизъюнкт D ∈ S инабор основных термов t1 , .

. . , tn , такие чтоI 6|= D[t1 , . . . , tn ]⇔Для каждой H-интерпретации I существуетосновной1 пример2 D 0 дизъюнкта D ∈ S, такой чтоI 6|= D 012D 0 не содержит переменныхD 0 = Dθ для некоторой подстановки θТеорема ЭрбранаРассмотрим такое множество дизъюнктов GS :D — основной пример какого-либо дизъюнкта из S;D ∈ GS ⇔существует H-интерпретация I, такая что I 6|= DТогдасистема дизъюнктов S противоречива⇔система дизъюнктов GS противоречиваТеорема ЭрбранаТеорема компактности Мальцева: Γ |= ϕ ⇔ существуетконечное подмножество Γ0 множества Γ, такое что Γ0 |= ϕСледствие: множество замкнутых формул Γ противоречивосуществует конечное противоречивое подмножество Γ0множества ΓПрименим это следствие к системе GS :множество GS противоречиво⇔существует конечное противоречивое подмножество G 0множества GSТолько что мы доказали теорему Эрбрана⇔Теорема ЭрбранаСистема дизъюнктов противоречива⇔Существует конечное противоречивое множествоосновных примеров дизъюнктов этой системыОсновной пример дизъюнкта не содержит кванторов ипредметных переменныхЗначит, конечная система основных примеров дизъюнктов —это (с небольшими техническими поправками) конечнаясистема булевых формулЗначит ли это, что (неразрешимая) проблема общезначимостиформул логики предикатов сведена к (NP-полной) проблемевыполнимости булевых формул?Нет: в теореме Эрбрана не говорится, как построитьподходящую систему основных примеров дизъюнктовТеорема ЭрбранаСистема дизъюнктов противоречива⇔Существует конечное противоречивое множествоосновных примеров дизъюнктов этой системыА зачем тогда нужна теорема Эрбрана?IДалее будет показано существование успешногорезолютивного вывода для произвольной конечнойпротиворечивой системы основных примеров дизъюнктов, иIна основании этого вывода будет построен успешныйрезолютивный вывод для произвольной противоречивойсистемы дизъюнктовТак будет обосновываться полнота метода резолюцийКонец лекции 8.