Ещё одни лекции В.А. Захарова, страница 13

. . , DN } — система дизъюнктов.Резолютивным выводом из системы дизъюнктов S называетсяконечная последовательность дизъюнктов, . . . , Dn ,D1 , D2 , . . . , Di , Di+1в которой для любого i, 1 ≤ i ≤ n, выполняется одно из трехусловий:1. либо Di — вариант некоторого дизъюнкта из S;2.

либо Di — резольвента дизъюнктов Dj и Dk , где j, k < i;3. либо Di — склейка дизъюнкта Dj , где j < i.Дизъюнкты D1 , D2 , . . . , Dn считаются резолютивновыводимыми из системы S.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.S = {D1 , D2 , D3 }D1 = P(x, f (y )) ∨ R(y ),D2 = ¬R(y ),D3 = ¬P(f (x), z) ∨ ¬P(y , y ).Резолютивный вывод из S1.2.3.4.5.6.D1D2D3D4D5D6= P(x1 , f (y1 )) ∨ R(y1 ), вариант дизъюнкта D1= ¬R(y2 ), вариант дизъюнкта D2= P(x3 , f (y3 )), резольвента дизъюнктов D1 , D2= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 ), вариант дизъюнкта D3= ¬P(f (x5 ), f (x5 )), склейка D4= , резольвента дизъюнктов D3 и D5Здесь — пустой дизъюнкт , тождественная ложь.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.А почему пустой дизъюнкт — это тождественная ложь?А потому, что каждый дизънкт D = L1 ∨ · · · ∨ Ln равносиленутверждению L1 ∨ · · · ∨ Ln ∨ false.Поэтому резольвентой дизъюнктов D1 = L ∨ false иD2 = ¬L ∨ false будет дизъюнкт D0 = false.Этот дизъюнкт не содержит ни одной литеры, и поэтомуназывается пустым дизънктом .РЕЗОЛЮТИВНЫЙ ВЫВОДОбратите внимание на то, что я постоянно переименовываюпеременные так, чтобы каждый дизъюнкт резолютивноговывода содержал свою индивидуальную систему переменных!Резолютивный вывод из S1.2.3.4.5.6.D1D2D3D4D5D6= P(x1 , f (y1 )) ∨ R(y1 )= ¬R(y2 )= P(x3 , f (y3 ))= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 )= ¬P(f (x5 ), f (x5 ))=Зачем это нужно?РЕЗОЛЮТИВНЫЙ ВЫВОДВсе дело в том, что все переменные дизъюнктов связаныкванторами ∀, и поэтому их имена можно достаточнопроизвольно изменять, полностью сохраняя смысл формул.Однако, случайное совпадение имен переменных (коллизия)может привести к тому, что резольвенту дизъюнктов построитьне удастся.Пусть S = {D1 = P(x), D2 = ¬P(f (x))}.1.

D1 = P(x)2. D2 =¬P(f (x))3. НОУ P(x), P(f (x)) = ∅,1. D1 = P(x1 )2. D2 = ¬P(f (x2 ))и поэтому D1 , D2не имеют резольвенты.резольвента D1 , D2 .3. D3 = Итак, наш девиз:НОВЫЙ ДИЗЪЮНКТ — НОВЫЕ ПЕРЕМЕННЫЕ.РЕЗОЛЮТИВНЫЙ ВЫВОДРезолютивный вывод называется успешным (или, по другому,резолютивным опровержением ), если этот вывод оканчиваетсяпустым дизъюнктом .В чем же состоит успех такого резолютивного вывода и чтопри этом опровергнуто?Успешный вывод — это свидетельство того, что системадизъюнктов S противоречива и опровергнуто предположениео ее выполнимости!Но это придется обосновать.КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАТеорема корректности резолютивного выводаЕсли из системы дизъюнктов S резолютивно выводим пустойдизъюнкт , то S — противоречивая система дизъюнктов.Доказательство теоремыПустой дизъюнкт тождественно ложен, т.е.

не имеет моделей.Покажем, что каждый дизъюнкт, резолютивно выводимый изS, является логическим следствием S. ТогдаS |= ,и это означает, что S также не имеет моделей, т.е. являетсяпротиворечивой системой.Остается доказать две леммы.КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАЛемма 1.Если D0 — резольвента дизъюнктов D1 и D2 , то D1 , D2 |= D0Доказательство леммы 1.D1 = D1 ∨L1 , D2 = D2 ∨¬L2 , θ ∈ НОУ(L1 , L2 ), D0 = (D1 ∨D2 )θТаким образом, L1 θ = L2 θ = L0 .Поэтому мы получаем следующие соотношенияD1 , D2 |= D1 θ,D1 , D2 |= D1 θ ∨ L1 θ,D1 , D2 |= D1 θ ∨ L0 ,D1 , D2 |= D1 θ ∨ D2 θ ∨ L0 ,D1 , D2 |= D2 θD1 , D2 |= D2 θ ∨ ¬L2 θD1 , D2 |= D2 θ ∨ ¬L0D1 , D2 |= D1 θ ∨ D2 θ ∨ ¬L0D1 , D2 |= D1 θ ∨ D2 θD1 , D2 |= D0Вот и все. КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАЛемма 2.Если D0 — склейка дизъюнкта D, то D |= D0 .Доказательство леммы 2.Самостоятельно.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙПример.Рассмотрим формулу ϕ∀x∀y ∃v ∀u(A(u, v ) → B(y , u))&(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ЗадачаПроверить, верно ли, что |= ϕ.РешениеМетодом резолюций.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 1.

Покажем, что формула ϕ1 = ¬ϕ противоречивая.∀y ∃v ∀u(A(u, v ) → B(y , u)) &ϕ1 = ¬∀x(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Исходная формула¬∀x∀y ∃v ∀u(A(u, v ) → B(y , u)) &(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Переименование переменных(A(u, v ) → B(y , u)) &¬∀x∀y ∃v ∀u(¬∃wA(w , u) → ∀zA(z, v ))→ ∃y B(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Удаление импликаций(¬A(u, v ) ∨ B(y , u)) &¬∀x¬∀y ∃v ∀u(¬¬∃wA(w , u) ∨ ∀zA(z, v ))∨ ∃y B(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Продвижение отрицаний(¬A(u, v ) ∨ B(y , u)) &∃x∀y ∃v ∀u(∃wA(w , u) ∨ ∀zA(z, v ))& ∀y ¬B(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2.

Приведем ϕ1 к ПНФ ϕ2 .Вынесение кванторовϕ2 =∃x∀y ∃v ∀u∃w ∀z∀y (¬A(u, v ) ∨ B(y , u)) &(A(w , u) ∨ A(z, v )) &¬B(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 3. Приведем ϕ2 к ССФ ϕ3 .ϕ3 =∀y ∀u∀z∀y (¬A(u, f (y )) ∨ B(y , u)) &(A(g (y , u), u) ∨ A(z, f (y ))) & ¬B(c, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 4.

Формирование системы дизъюнктов Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1. D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))),5. D5 = ¬B(c, y5 ),6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1. D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ), (вариант D1 )2.

D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))),5. D5 = ¬B(c, y5 ),6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1. D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )), (вариант D2 )3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))),5. D5 = ¬B(c, y5 ),6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5.

Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1. D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )), (склейка D2 )4. D4 = B(y4 , g (y4 , f (y4 ))),5. D5 = ¬B(c, y5 ),6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1.

D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))), (резольвента D1 и D3 )5. D5 = ¬B(c, y5 ),6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1.

D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))),5. D5 = ¬B(c, y5 ), (вариант D3 )6. D6 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =D1 = ¬A(u, f (y )) ∨ B(y , u),D2 = A(g (y , u), u) ∨ A(z, f (y )), D3 = ¬B(c, y )1. D1 = ¬A(u1 , f (y1 )) ∨ B(y1 , u1 ),2. D2 = A(g (y2 , u2 ), u2 ) ∨ A(z2 , f (y2 )),3. D3 = A(g (y3 , f (y3 )), f (y3 )),4. D4 = B(y4 , g (y4 , f (y4 ))),5.

D5 = ¬B(c, y5 ),6. D6 = . (резольвента D4 и D5 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЗаключение. Успешный резолютивный вывод из Sϕ означает,что Sϕ — противоречивая система дизъюнктов.Значит, ϕ1 = ¬ϕ — невыполнимая формула.Значит, ϕ — общезначимая формула,|= ϕ.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙВопрос полнотыА можно ли таким способом проверять общезначимость любыхформул?Этот вопрос может быть уточнен так:1. Верно ли, что для любой общезначимой формулы ϕможно построить успешный резолютивный вывод изсоответствующей системы дизъюнктов Sϕ ?2. Верно ли, что в том случае, когда формулы ϕнеобщезначима (система дизъюнктов Sϕ выполнима), мысможем каким-то образом обнаружить невозможностьпостроения успешного резолютивного вывода?КОНЕЦ ЛЕКЦИИ 9.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

ЗахаровЛекция 10.Полнота резолютивного вывода.Применение метода резолюций.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАТеорема о полноте резолютивного выводаЕсли S — противоречивая система дизъюнктов, то из Sрезолютивно выводим пустой дизъюнкт .Доказательство.Если S — противоречивая система дизъюнктов, то согласнотеореме Эрбрана существует конечная противоречивая системаS основных примеров дизъюнктов из S.

Поэтому мы1. Вначале покажем, что из противоречивой системы основныхпримеров дизъюнктов S можно резолютивно вывести пустойдизъюнкт .2. А затем на основе этого вывода построим резолютивныйвывод пустого дизъюнкта из самой системы S.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма об основных примерах дизъюнктовЕсли S — конечная противоречивая система основныхпримеров дизъюнктов, то из S резолютивно выводим пустойдизъюнкт .Доказательство леммы.Индукцией по числу N различных основных атомов в системедизъюнктов S .Базис (N = 0). Система S противоречива. Значит, S = ∅.Но в S нет ни одного атома.

Значит, в S содержится толькопустой дизъюнкт . И он резолютивно выводим из S .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Индуктивный переход (N + 1 → N). Рассмотримпроизвольный основной атом A0 , входящий в составдизъюнктов из S , и разобьем систему S на три части: 1 ∨ A0 };1. S = {D : D ∈ S , D = D2.3.1S2S3 2 ∨ ¬A0 }.= {D : D ∈ S , D = D= {D : D ∈ S , A0 ∈/ D};Построим все резольвенты по контрарной паре A0 , ¬A01 ∨ D 2 : D1 = D 1 ∨ A0 ∈ S , D2 = D 2 ∨ ¬A0 ∈ S }S0 = {D12и покажем, что множество дизъюнктов S = S0 ∪ S3противоречиво.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.'' 1 ∨ A0D&&S1$' 2 ∨ ¬A0D%&$S2$'S $S3нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.''S1$' 1 ∨ A0DBB$S2 2 ∨ ¬A0D$'S $S3нет атомов A0&%&%&%B&%BB$'BS$$''BS3B S0BNB1 ∨ D2Dрезольвенты&&нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Рассмотрим произвольную интерпретацию I .Для определенности будем полагать, что I |= A0(если I |= ¬A0 , то рассуждения будут аналогичны).Покажем, что I |= S .Т.