LectLog10 (1158002)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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

Система S 0 противоречива. Значит, S 0 6= ∅.Но в S 0 нет ни одного атома. Значит, в S 0 содержится толькопустой дизъюнкт . И он резолютивно выводим из S 0 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Индуктивный переход (N + 1 → N). Рассмотримпроизвольный основной атом A0 , входящий в составдизъюнктов из S 0 , и разобьем систему S 0 на три части:b 1 ∨ A0 };1. S 0 = {D : D ∈ S 0 , D = D2.3.1S20S30b 2 ∨ ¬A0 }.= {D : D ∈ S 0 , D = D= {D : D ∈ S 0 , A0 ∈/ D};Построим все резольвенты по контрарной паре A0 , ¬A0b1 ∨ Db 2 : D1 = Db 1 ∨ A0 ∈ S 0 , D2 = Db 2 ∨ ¬A0 ∈ S 0 }S00 = {D12и покажем, что множество дизъюнктов S 00 = S00 ∪ S30противоречиво.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.''b 1 ∨ A0D&&S01$'b 2 ∨ ¬A0D%&$S02$'S0 $S03нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.''S01$$'b 1 ∨ A0DS02b 2 ∨ ¬A0DB$'S0 $S03нет атомов A0B&%&%&%B&%BB'$00BS'$'$B0S03B S0BNBb1 ∨ Db2Dрезольвенты&&нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Рассмотрим произвольную интерпретацию I .Для определенности будем полагать, что I |= A0(если I |= ¬A0 , то рассуждения будут аналогичны).Покажем, что I 6|= S 00 .Т.

к. S 0 противоречивая система, верно I 6|= S10 ∪ S20 ∪ S30 .b ∨ A0 }, верно I |= S 0 .Т. к. I |= A0 и S10 = {D : D ∈ S 0 , D = D1Значит, I 6|= S20 ∪ S30 .Возможны два варианта.Вариант 1. I 6|= S30 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Рассмотрим произвольную интерпретацию I .Для определенности будем полагать, что I |= A0(если I |= ¬A0 , то рассуждения будут аналогичны).Покажем, что I 6|= S 00 .Т. к.

S 0 противоречивая система, верно I 6|= S10 ∪ S20 ∪ S30 .b ∨ A0 }, верно I |= S 0 .Т. к. I |= A0 и S10 = {D : D ∈ S 0 , D = D1Значит, I 6|= S20 ∪ S30 .Возможны два варианта.Вариант 1. I 6|= S30 . Тогда I 6|= S 00 , что и требовалось.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01$'b 1 ∨ A0D&&$S02$'b 2 ∨ ¬A0D%&''b1 ∨ Db2D&&S0 $S03нет атомов A0%&%%$S00'$S00 $S03нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01true$'b 1 ∨ A0D&&$S02$'b 2 ∨ ¬A0D%&''b1 ∨ Db2D&&S0 $S03нет атомов A0%&%%$S00'$S00 $S03нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01true$'b 1 ∨ A0DВариант 1.S02b 2 ∨ ¬A0D$S0 $S03$'нет атомов A0I 6|= D&&%&''b1 ∨ Db2D&&%&%%$S00'$S00 $S03нет атомов A0&%%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01true$'b 1 ∨ A0DВариант 1.S02$'b 2 ∨ ¬A0D$S0 $S03нет атомов A0I 6|= D&&%&''b1 ∨ Db2D&&%&%%$S00$'S00 $S03нет атомов A0I 6|= D%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2. I 6|= S20 .b 2 ∨ ¬A0 ∈ S 0 , чтоЗначит, существует такой дизъюнкт D2b 2 (почему? ).b 2 ∨ ¬A0 .

Следовательно, I 6|= DI 6|= DРассмотрим теперь интерпретацию I 0 , которая отличается от Iтолько тем, что I 0 6|= A0 .Т. к. I 0 6|= S10 ∪ S20 ∪ S30 (ведь S 0 противоречивая),b ∨ ¬A0 } и I 0 |= ¬A0 ),I 0 |= S20 (ведь S20 = {D : D ∈ S 0 , D = D00I |= S3 (а иначе мы бы имели вариант 1, ведь A0 ∈/ S30 ),верно I 0 6|= S10 .b 1 ∨ A0 ∈ S 0 , чтоЗначит, существует такой дизъюнкт D1b 1 ∨ A0 . Следовательно, I 0 6|= Db 1 . А поскольку A0 ∈b1, а II 0 6|= D/D0bотличается от I только на атоме A0 , верно I 6|= D1 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01true$'b 1 ∨ A0D&&Вариант 2.S02b 2 ∨ ¬A0Db1 ∨ Db2D&&true$$S03нет атомов A0%&''$'S0%&%%$S00$'S00 $S03нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01trueВариант 2.$'b 1 ∨ A0DS02b 2 ∨ ¬A0D$'true$S0$S03нет атомов A0b2I 6|= D&&%&''b1 ∨ Db2D&&%&%%$S00$'S00 $S03нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI |= A0''S01trueВариант 2.$'b 1 ∨ A0DS02b 2 ∨ ¬A0D$'true$S0$S03нет атомов A0b2I 6|= D&&%&''%%$S00b1 ∨ Db2D&&%&b2I 6|= D$'S00 $S03нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI0 6|= A0''S01$'b 1 ∨ A0DВариант 2.S02b 2 ∨ ¬A0D$'true$S0$S03нет атомов A0b2I 6|= D&&%&''%%$S00b1 ∨ Db2D&&%&b2I 6|= D$'S00 $S03нет атомов A0%&%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI0 6|= A0''S01$'S02b 1 ∨ A0Db 2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&''$'trueS00нет атомов A0%&b2I 6|= D$'%%S00 $S03нет атомов A0%&$S0 $S03$b1 ∨ Db2D&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI0 6|= A0''S01$'S02b 1 ∨ A0Db 2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&''b1I0 6|= D$'trueS00нет атомов A0%&b2I 6|= D$'%%S00 $S03нет атомов A0%&$S0 $S03$b1 ∨ Db2D&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАI0 6|= A0''S01$'S02b 1 ∨ A0Db 2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&''$'trueS00нет атомов A0%&b1 ∨ Db2I 6|= D$'%%S00 $S03нет атомов A0%&$S0 $S03$b1 ∨ Db2D&&Вариант 2.%%ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.b 1 и I 6|= Db 2 , верно I 6|= Db1 ∨ Db2.Т.к.

I 6|= Db1 ∨ Db 2 — это резольвента дизъюнктовОстается заметить, что D00bbb1 ∨ Db2 ∈ S 0D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.b 1 и I 6|= Db 2 , верно I 6|= Db1 ∨ Db2.Т.к. I 6|= Db1 ∨ Db 2 — это резольвента дизъюнктовОстается заметить, что D00bbb1 ∨ Db2 ∈ S 0D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0Следовательно, I 6|= S00 .

Тогда I 6|= S 00 , что и требовалось.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы.Вариант 2.b 1 и I 6|= Db 2 , верно I 6|= Db1 ∨ Db2.Т.к. I 6|= Db1 ∨ Db 2 — это резольвента дизъюнктовОстается заметить, что D00bbb1 ∨ Db2 ∈ S 0D2 ∨ ¬A0 ∈ S2 и D1 ∨ A0 ∈ S1 , и поэтому D0Следовательно, I 6|= S00 .

Тогда I 6|= S 00 , что и требовалось.Итак, в обоих случаях I 6|= S 00 . Т. к. I — произвольнаяинтерпретация, приходим к заключению о том, что системадизъюнктов S 00 = S00 ∪ S30Iпротиворечивая,Iполучена из S 0 при помощи правила резолюции,Iне содержит атома A0 .Индуктивный переход завершен, и лемма доказана.ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеПусть D1 и D1 — два дизъюнкта, и при этом VarD1 ∩ VarD2 = ∅.Пусть D10 = D1 θ и D20 = D2 θ — два основных примера этихдизъюнктов D1 и D1 .Пусть D00 — резольвента дизъюнктов D10 и D20 .Тогда из дизъюнктов D1 и D2 резолютивно выводим дизъюнктD0 , основным примером которой является дизъюнкт D00 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2??D10 = D1 θD20 = D2 θ@@@@R@D00ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2@@@@R@D0??D10 = D1 θD20 = D2 θ@@@@R@?D00ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАЛемма о подъемеD1D2@@@@R@D0?6D10 = D1 θ?D20 = D2 θ@@@@R@?D00ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеПусть L00 , ¬L00 — это контрарная пара литер, по которой былапостроена резольвента D00 дизъюнктов D10 и D20 .b 0 ∨ L0 ,D10 = D10b 0 ∨ ¬L0 ,D20 = D20b0 ∨ Db0.D00 = D12Поскольку VarD1 ∩ VarD2 = ∅, подстановку θ можно разделитьна две половины θ1 , θ2 так, чтоθ = θ1 ∪ θ2 , Domθ1 ⊆ VarD1 , Domθ2 ⊆ VarD2 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеD1D2??b 0 ∨ L0 = D1 θ1D01b 0 ∨ ¬L0 = D2 θ2D20@@@@R@b0 ∨ Db0D12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеПоскольку D10 = D1 θ1 , литера L00 является основным примеромнекоторых литер L11 , L12 , .

. . , L1k1 , входящих в составдизъюнкта D1 , т.е.L00 = L11 θ = L11 θ1 = · · · = L1k1 θ1 .Аналогично, литера ¬L00 является основным примеромнекоторых литер ¬L21 , ¬L22 , . . . , ¬L2k2 , входящих в составдизъюнкта D2 , т. е.¬L00 = ¬L21 θ2 = ¬L22 θ2 = · · · = ¬L2k2 θ2 .Значит,b 1 ∨ L11 ∨ L12 ∨ · · · ∨ L1kD1 = D1b 2 ∨ ¬L21 ∨ ¬L22 ∨ · · · ∨ ¬L2kD2 = D2ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеb 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2b 1 ∨ L11 ∨ · · · ∨ L1kD1θ1θ2@@@ @R @@R@@@@R@b 0 ∨ L0 = D1 θ1D10R@b 0 ∨ ¬L0 = D2 θ2D20@@@@R@b0 ∨ Db0D12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеТак как L00 = L11 θ = L12 θ1 = · · · = L1k1 θ1 , литерыL11 , L12 , . .

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций