Лекция 17. Отрицание в логическом программировании. Оператор not ... (1161888)

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

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

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 17.Отрицание в логическомпрограммировании.Оператор not.Встроенные предикаты ифункции.Оператор вычисления значений.Модификация баз данных.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИОтрицание ¬ — это очень полезная логическая связка. Частомы обращаемся с вопросами, используя отрицание.ПримерP : птица(орел) ←;птица(воробей) ←;птица(пингвин) ←;летает(орел) ←;летает(воробей) ←;летает(самолет) ←;Сформулируем вопрос: какая птица не летает?G : ? птица(X ), ¬летает(X )Какой ответ мы ожидаем получить на этот запрос?ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИПримерС точки зрения декларативной семантики, для полученияответа на этот запрос нужно выяснить, выполняется лилогическое следованиеP |= ∃X (птица(X )&¬летает(X )),где P = {птица(орел), птица(воробей), птица(пингвин),летает(орел), летает(воробей), летает(самолет)}Оно не выполняется, т.

к.BP |= P, BP 6|= ∃X (птица(X )&¬летает(X )).Значит, ответ на этот запрос должен быть отрицательным:такой птицы нет .ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИПримерОднако в обыденной жизни мы в таких случаях даем совсемдругой ответ.Обнаружив, что в нашей базе знаний Pесть сведение птица(пингвин) инет никаких сведений о том, что летает(пингвин),мы отвечаем:«Насколько позволяет судить наша база знаний, нелетающаяптица — это пингвин».В юрипруденции такой подход к решению вопроса о виновностичеловек называется презумпцией невиновности :в случае отсутствия свидетельств виновностичеловек считается невиновным.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИМы можем распространить принцип презумпции невиновностии на логические программы.Допущение Замкнутости МираПусть имеется некоторое непротиворечивое множествозамкнутых формул Γ (например, хорновская логическаяпрограмма) и замкнутая формула ϕ (например, запрос илиотдельная подцель).Тогда формула ¬ϕ является логическим следствием множестваΓ в допущении замкнутости мираΓ |=CWA ¬ϕ,если неверно, что ϕ логически следует из Γ, т.

е. Γ 6|= ϕ.Здесь CWA — аббревиатура C losed W orld A ssumption.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИСуть Допущения Замкнутости Мира (CWA) состоит в том, чтопри извлечении CWA-логических следствий из базы знаний Γ(|=CWA ) нужно рассматривать не все модели для Γ, а толькотакую минимальную модель, в которой истинными являютсяодни лишь классические следствия (|=) из Γ.Такая минимальная модель существует, вообще говоря, невсегда (например, если Γ = {A ∨ B}).Но в случае хорновских логических программ, минимальноймоделью для программы P является наименьшая эрбрановскаямодель MP .ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИОбратимся к орнитологическому примеру.ПримерP = {птица(орел), птица(воробей), птица(пингвин),летает(орел), летает(воробей), летает(самолет)}ϕ= птица(пингвин) & ¬летает(пингвин)ТогдаP |=CWA птица(пингвин), поскольку MP |= птица(пингвин),P |=CWA ¬летает(пингвин), поскольку MP 6|= летает(пингвин).Значит, P |=CWA птица(пингвин) & ¬летает(пингвин).ОПЕРАТОР notИтак, теперь к логическим программам можно обращаться сзапросами, содержащими отрицания подцелей, идекларативная семантика умеет разумно обращаться с такимотрицательными подцелями.Нам остается научить этому обращению компьютер, т.

е.ввести в операционную семантику правила для обработкиотрицательных подцелей.Однако здесь нас ожидает неприятный сюрприз.ОПЕРАТОР notПредположим, что имеется запрос G : ?¬C0 к программе P.Чтобы получить утвердительный ответ на запрос G (т. е.доказать, что P |=CWA ¬C0 ), интерпретатор должен проверить,что MP 6|= C0 .Для этого интерпретатор должен убедиться, что запросG 0 : ?C0 к программе P не имеет ни одного успешноговычисления.Но эта задача является алгоритмически неразрешимой(почему? ).Да потому, что к ней сводится проблема останова машинТьюринга.Следовательно, никакой интерпретатор логических программне может гарантировать получение утвердительного ответа назапрос G : ?¬C0 даже в том случае, если этот ответ существует.ОПЕРАТОР notАлгоритмическая неразрешимость проблемы существования(отсутствия) успешного вычисления логических программ —это непреодолимое препятствие на пути создания такойоперационной семантики, которая была бы адекватнадекларативной семантике в рамках Допущения ЗамкнутостиМира.Можно лишь построить такой интерпретатор (операционнойсемантики), который как можно лучше соответствует CWA приобращении с отрицательными подцелями ¬C0 .Для этого в язык логического программирования был введенспециальный (встроенный) оператор not.ОПЕРАТОР notАргументами оператора not являются атомы.Для вычисления ответов на запрос ? not(C0 ) вводится правилоSLDNF-резолюции (N ot as F ailure), которое определяетсяследующим образом.Правило SLDNF-резолюцииПусть имеется запрос G0 : ? not(C0 ), C1 , .

. . , Cn к программе P.Для вычисления SLDNF-резольвенты G11. формируется запрос G 0 : ? C0 к программе P;2. проводится построение (обход) дерева вычислений Tзапроса G 0 : ? C0 ;3. в зависимости от устройства дерева T возможен один изтрех исходов.ОПЕРАТОР notПравило SLDNF-резолюцииВариант 1: Успех.Дерево T конечно, и все его ветви (SLD-резолютивныевычисления) являются тупиковыми.Тогда запрос G0 : ? not(C0 ), C1 , . .

. , Cn имеетSLDNF-резольвенту G1 = ? C1 , . . . , Cn , которая получается сиспользованием пустой подстановки ε.G 0 : ? C0t@T @t⇒@failureG0 : ? not(C0 ), C1 , . . . , Cn@ε?tG1 : ? C1 , . . . , CnОПЕРАТОР notОперационная семантика оператор notВариант 2: Неудача.При построении (обходе) дерева T было обнаруженоуспешное вычисление.Тогда запрос G0 : ? not(C0 ), C1 , .

. . , Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсятупиковым .G 0 : ? C0G0 : ? not(C0 ), C1 , . . . , Cnt@T @t⇒@@failureR@failureОПЕРАТОР notОперационная семантика оператор notВариант 3: Бесконечное вычисление.Дерево T бесконечно и при его построении (обходе) небыло обнаружено успешных вычислений.Тогда запрос G0 : ? not(C0 ), C1 , . . .

, Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсябесконечным («сингулярная бесконечность»).G 0 : ? C0t@T @t⇒@failureG0 : ? not(C0 ), C1 , . . . , Cn@R∞@∞ОПЕРАТОР notОперационная семантика оператор notВариант 3: Бесконечное вычисление.Дерево T бесконечно и при его построении (обходе) небыло обнаружено успешных вычислений.Тогда запрос G0 : ? not(C0 ), C1 , . . . , Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсябесконечным («сингулярная бесконечность»).Условие существования бесконечного вычисления запросаnot(C0 ) описано не вполне строго, поскольку обнаружениеуспешного вычисления существенно зависит от стратегииобхода дерева SLD-резолютивных вычислений.

Так, например,стандартная стратегия обхода в глубину может не обнаружитьсуществующего успешного вычисления (почему? ).ОПЕРАТОР notТеорема (корректности SLDNF-резолюции)Если запрос G : ? not(C0 ) к хорновской логической программеP имеет успешное SLDNF-резолютивное вычисление, тоP |=CWA ¬∃y C0 .ДоказательствоСамостоятельно .А вот обратное утверждение (теорема полноты) дляSLDNF-резолютивного вычисления будет уже неверно.ОПЕРАТОР notПример.Рассмотрим программу поиска всех тех букв X слова L0 ,которые не содержатся в слове L00 .P : S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ← ;E (X , Y L) ← E (X , L);..и обратимся к ней с запросом.. ..G0 : ? S(X , a b nil, b c nil)...S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..?S(X , a b t nil, b c nil)(1)(2)(3)..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3)..

..?S(X , a b t nil, b c nil)(1).. ..?t?E (X , a.b .nil),not(E (X , b .c .nil))θ1 = {X1 /X , L0 /aL00 /bbcnil,nil}..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L0 /aL00 /bnil}(2)t..?not(E (a, b c nil))bcnil,nil}..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L0 /aL00 /bbcnil,nil}..?E (a, b tc nil)..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3)..

..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L0 /aL00 /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L0 /aL00 /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)?t?E (a, nil)..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3)..

..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L0 /aL00 /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)?t?E (a, nil)failure..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),(X , b .c .nil)). ?t?E (Xnot(E(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L0 /aL00 /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)6?t?E (a, nil)failure..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil)..

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

Тип файла PDF

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

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

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