Ещё одни лекции В.А. Захарова (1158033), страница 14
Текст из файла (страница 14)
к. S противоречивая система, верно I |= S1 ∪ S2 ∪ S3 . ∨ A0 }, верно I |= S .Т. к. I |= A0 и S1 = {D : D ∈ S , D = D1Значит, I |= S2 ∪ S3 .Возможны два варианта.Вариант 1. I |= S3 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Рассмотрим произвольную интерпретацию I .Для определенности будем полагать, что I |= A0(если I |= ¬A0 , то рассуждения будут аналогичны).Покажем, что I |= S .Т. к. S противоречивая система, верно I |= S1 ∪ S2 ∪ S3 . ∨ A0 }, верно I |= S .Т.
к. I |= A0 и S1 = {D : D ∈ S , D = D1Значит, I |= S2 ∪ S3 .Возможны два варианта.Вариант 1. I |= S3 . Тогда I |= S , что и требовалось.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1$' 1 ∨ A0D&&$S2$' 2 ∨ ¬A0D%&''1 ∨ D2D&&S $S3нет атомов A0%&%%$S0$'S $S3нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1true$' 1 ∨ A0D&&$S2$' 2 ∨ ¬A0D%&''1 ∨ D2D&&S $S3нет атомов A0%&%%$S0$'S $S3нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1true$' 1 ∨ A0DВариант 1.S2 2 ∨ ¬A0D$S $S3$'нет атомов A0I |= D&&%&''1 ∨ D2D&&%&%%$S0$'S $S3нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1true$' 1 ∨ A0DВариант 1.S2$' 2 ∨ ¬A0D$S $S3нет атомов A0I |= D&&%&''1 ∨ D2D&&%&%%$S0$'S $S3нет атомов A0I |= D%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.
I |= S2 . 2 ∨ ¬A0 ∈ S , чтоЗначит, существует такой дизъюнкт D2 2 ∨ ¬A0 . Следовательно, I |= D 2 (почему? ).I |= DРассмотрим теперь интерпретацию I , которая отличается от Iтолько тем, что I |= A0 .Т. к. I |= S1 ∪ S2 ∪ S3 (ведь S противоречивая), ∨ ¬A0 } и I |= ¬A0 ),I |= S2 (ведь S2 = {D : D ∈ S , D = DI |= S3 (а иначе мы бы имели вариант 1, ведь A0 ∈/ S3 ),верно I |= S1 . 1 ∨ A0 ∈ S , чтоЗначит, существует такой дизъюнкт D1 1 ∨ A0 . Следовательно, I |= D 1 . А поскольку A0 ∈1, а II |= D/Dотличается от I только на атоме A0 , верно I |= D1 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1true$' 1 ∨ A0D&&Вариант 2.S2 2 ∨ ¬A0D1 ∨ D2D&&true$$S3нет атомов A0%&''$'S%&%%$S0$'S $S3нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1trueВариант 2.$' 1 ∨ A0DS2 2 ∨ ¬A0D$'true$S$S3нет атомов A02I |= D&&%&''1 ∨ D2D&&%&%%$S0$'S $S3нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1trueВариант 2.$' 1 ∨ A0DS2 2 ∨ ¬A0D$'true$S$S3нет атомов A02I |= D&&%&%%$''S01 ∨ D2D&&%&2I |= D$'S $S3нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1$' 1 ∨ A0DВариант 2.S2 2 ∨ ¬A0D$'true$S$S3нет атомов A02I |= D&&%&%%$''S01 ∨ D2D&&%&2I |= D$'S $S3нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1$'S2 1 ∨ A0D 2 ∨ ¬A0D1I |= D2I |= D&&%&$'trueS0нет атомов A0%&1 ∨ D2D2I |= D$'%%S $S3нет атомов A0%&$S $S3$''&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1$'S2 1 ∨ A0D 2 ∨ ¬A0D1I |= D2I |= D&&%&S01 ∨ D2D1I |= D$'trueнет атомов A0%&2I |= D$'%%S $S3нет атомов A0%&$S $S3$''&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S1$'S2 1 ∨ A0D 2 ∨ ¬A0D1I |= D2I |= D&&%&''$'trueS0нет атомов A0%&1 ∨ D2I |= D$'%%S $S3нет атомов A0%&$S $S3$1 ∨ D2D&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.
2 , верно I |= D1 ∨ D2. 1 и I |= DТ.к. I |= D 2 — это резольвента дизъюнктов1 ∨ DОстается заметить, что D1 ∨ D2 ∈ S D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2. 2 , верно I |= D1 ∨ D2. 1 и I |= DТ.к. I |= D 2 — это резольвента дизъюнктов1 ∨ DОстается заметить, что D1 ∨ D2 ∈ S D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0Следовательно, I |= S0 . Тогда I |= S , что и требовалось.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.
2 , верно I |= D1 ∨ D2. 1 и I |= DТ.к. I |= D 2 — это резольвента дизъюнктов1 ∨ DОстается заметить, что D1 ∨ D2 ∈ S D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0Следовательно, I |= S0 . Тогда I |= S , что и требовалось.Итак, в обоих случаях I |= S . Т.
к. I — произвольнаяинтерпретация, приходим к заключению о том, что системадизъюнктов S = S0 ∪ S3противоречивая,получена из S при помощи правила резолюции,не содержит атома A0 .Индуктивный переход завершен, и лемма доказана.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеПусть D1 и D1 — два дизъюнкта, и при этом VarD1 ∩ VarD2 = ∅.Пусть D1 = D1 θ и D2 = D2 θ — два основных примера этихдизъюнктов D1 и D1 .Пусть D0 — резольвента дизъюнктов D1 и D2 .Тогда из дизъюнктов D1 и D2 резолютивно выводим дизъюнктD0 , основным примером которой является дизъюнкт D0 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2??D1 = D1 θD2 = D2 θ@@@@R@D0ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2@@@@R@D0??D1 = D1 θD2 = D2 θ@@@@?R@D0ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2@@@@R@D0?D1 = D1 θ6@@@@?R@D0?D2 = D2 θПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеПусть L0 , ¬L0 — это контрарная пара литер, по которой былапостроена резольвента D0 дизъюнктов D1 и D2 .
∨ L ,D1 = D10 ∨ ¬L ,D2 = D20 ∨ D.D0 = D12Поскольку VarD1 ∩ VarD2 = ∅, подстановку θ можно разделитьна две половины θ1 , θ2 так, чтоθ = θ1 ∪ θ2 , Domθ1 ⊆ VarD1 , Domθ2 ⊆ VarD2 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеD1D2? ∨ L = D1 θ1D10@@? ∨ ¬L = D2 θ2D20@@R@ ∨ DD12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеПоскольку D1 = D1 θ1 , литера L0 является основным примеромнекоторых литер L11 , L12 , . .
. , L1k1 , входящих в составдизъюнкта D1 , т.е.L0 = L11 θ = L11 θ1 = · · · = L1k1 θ1 .Аналогично, литера ¬L0 является основным примеромнекоторых литер ¬L21 , ¬L22 , . . . , ¬L2k2 , входящих в составдизъюнкта D2 , т. е.¬L0 = ¬L21 θ2 = ¬L22 θ2 = · · · = ¬L2k2 θ2 .Значит, 1 ∨ L11 ∨ L12 ∨ · · · ∨ L1kD1 = D1 2 ∨ ¬L21 ∨ ¬L22 ∨ · · · ∨ ¬L2kD2 = D2ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъеме 1 ∨ L11 ∨ · · · ∨ L1kD1@ 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2θ1@@ @R@R@@@R@ ∨ L = D1 θ1D10θ2@@R@ ∨ ¬L = D2 θ2D20@@@@R@ ∨ DD12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеТак как L0 = L11 θ = L12 θ1 = · · · = L1k1 θ1 , литерыL11 , L12 , .
. . , L1k1 унифицируемы. Значит, они имеют НОУ η1 ,т. е.η1 ∈ НОУ(L11 , L12 , . . . , L1k1 ),θ1 = η1 ρ1 .Значит D1 η1 — склейка дизъюнкта D1 по литерамL11 , L12 , . . . , L1k1 , и при этом D1 = D1 θ1 = (D1 η1 )ρ1 — основнойпример склейки D1 η2 .Аналогично, литеры ¬L21 , ¬L22 , . . . , ¬L2k2 имеют НОУ η2 .Тогда D2 η2 — склейка дизъюнкта D2 по литерам¬L21 , ¬L22 , . . .
, ¬L2k2 , и при этом D2 = D2 θ2 = (D1 η2 )ρ2 —основной пример склейки D2 η2 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъеме 1 ∨ L11 ∨ · · · ∨ L1kD1@ @η1 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2@ @R @@R@ 1 η1 ∨ L11 η1 = D1 η1Dρ1?? ∨ L = D1 η1 ρ1D10@@@@R@ ∨ DD12R@@R@ 2 η2 ¬ ∨ L21 η2 = D2 η2Dρ2?? ∨ ¬L = D2 η2 ρ2D20ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеСогласно нашей привычке переименовывать переменные,дизъюнкты-склейки D1 η1 и D2 η2 содержат разные наборыпеременных. Поэтому Domρ1 ∩ Domρ2 = ∅, и существуетподстановка ρ = ρ1 ∪ ρ2 :(L11 η1 )ρ = (L11 η1 )ρ1 ,(L21 η2 )ρ = (L21 η2 )ρ2L0Так как= L11 η1 ρ1 и ¬L0 = ¬L21 η2 ρ2 , верно(L11 η1 )ρ = (L21 η2 )ρ, т. е.
литеры L11 η1 и L21 η2 унифицируемы.Значит, они имеют НОУ λ, т. е.λ ∈ НОУ(L11 η1 , L21 η2 ), ρ = λμ. 1 η1 ∨ L11 η1 иПоэтому дизъюнкты-склейки D1 η1 = D 2 η2 ∨ ¬L21 η2 имеют резольвенту D0 = (D 1 η1 ∨ D 2 η2 )λ,D2 η2 = Dи при этом ∨ D = D 1 η1 ρ ∨ D 2 η2 ρ = (D 1 η1 ∨ D 2 η2 )λμ = D0 μ.D0 = D12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъеме 1 ∨ L11 ∨ · · · ∨ L1kD1@ @η1 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2@ @R @@R@R@@R@ 1 η1 ∨ L11 η1 = D1 η1 2 η2 ∨ ¬L21 η2 = D2 η2DDXXXXXX λ ρρ9z X 2 η2 )λ 1 η1 ∨ D??(DD1 ∨ L0 = D1 η1 ρD2 ∨ ¬L0 = D2 η2 ρ@μ@@@?R@ ∨ DD12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеТаким образом, из дизъюнктов D1 и D2 резолютивно выводимдизъюнкт D0 , основным примером которого являнтся D0 .Что и требовалось доказать в лемме о подъеме.Завершение доказательства теоремы полноты.Мы показали, что1.
Противоречивая система дизъюнктов S имеет конечнуюпротиворечивую систему S основных примеров (теоремаЭрбрана ).2. Из противоречивой системы основных примеровдизъюнктов S можно резолютивно вывести пустойдизъюнкт (лемма об основных примерах ).3. Если резолютивно выводим из системы основныхпримеров дизъюнктов S , то резолютивно выводим изисходной системы дизъюнктов S (лемма о подъеме ). ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙМетод резолюций корректен, полон, алгоритмизуем.Но как пользоваться им для решенияпрактических задач?ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙВот подходящая логическая задачаИзвестно, что Даша любит Сашу, а Саша любит пиво, а Паша любит пиво и всех тех, ктолюбит то, что любит Паша.Вопрос: кто любит Дашу?ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.Вначале сформулируем задачу на языке логики предикатов.Сформируем алфавит, состоящий из:Константы Даша ,Константы Саша ,Константы Паша ,Константы пиво ,Предикатного символа L(2) : «L(x, y ) — x любит y ».ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.Далее запишем условия задачи на языке логики предикатов.Даша любит Сашу:ϕ1 : L(Даша, Саша),а Саша любит пиво:ϕ2 : L(Саша, пиво),а Паша любит пиво и всех тех, кто любит то, что любитПаша:ϕ 3 & ϕ4 ,ϕ3 : L(Паша, пиво)ϕ4 : ∀x (∃y (L(Паша, y ) & L(x, y )) → L(Паша, x)).Кто любит Дашу? :ϕ0 : ∃z L(z, Даша).Формулировка задачи.Проверить, верно ли, что{ϕ1 , ϕ2 , ϕ3 , ϕ4 } |= ϕ0 .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
