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

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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)..