LectLog14 (1158007)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 14.Полнота операционной семантикилогических программ.Оператор непосредственногоследования.Теоремы полноты.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММПроблема полнотыПусть θ — правильный ответ на запрос G0 к хорновскойлогической программе P, т.
е. P |= ∀z G0 θ.Существует ли такое успешное SLD-резолютивное вычисление,порожденное запросом G0 к программе P(Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , ),которое вычисляет ответ θ, т. е. θ = (θ1 θ2 . . . θn )|VarG0 ?Начнем изучение этого вопроса с более простой задачи. ПустьC0 — основной атом (т. е. VarC0 = ∅),G0 = ?C0 ,ε — правильный ответ на запрос ?C0 к программе P.Существует ли успешное SLD-резолютивное вычисление,порожденное запросом ?C0 к программе P?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИОпределение (множество успехов).Множеством успехов — хорновской логической программы Pназывается множество SuccP всех тех основных атомов C0 ,для которых запрос G0 = ?C0 к программе P порождаетуспешное SLD-резолютивное вычисление.Как следует из теоремы корректности операционной семантикии теоремы об основном правильном ответе ,C0 ∈ SuccP ⇒ P |= C0 ⇒ C0 ∈ MP .Значит, SuccP ⊆ MP(т.
е. программа успешно вычисляет вычисляетутвердительный ответ на вопрос ?C0 только в том случае,когда утверждение C0 истинно в наименьшей H-модели).А верно ли обратное включение SuccP ⊇ MP(все, что логически следует из программы можно вычислить)?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИНаименьшаяэрбрановская модель$'MPGt0 =?C0&%ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИНаименьшаяэрбрановская модель$'Нужно построитьMPвычислениеGt0 =?C0D j1G1 t &9D j2JJ^ t9G2JD j3rG3 t9rJJr^rrD jnr t9%ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЧтобы запрос G0 =?C0 мог «отыскать путь» к пустому запросу (успешное вычисление) в наименьшей модели MP , намнужно ввести в множестве основных атомов MP какие-нибудьориентиры (систему координат), руководствуясь которымиможно вывести из запроса G0 пустой запрос .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЧтобы запрос G0 =?C0 мог «отыскать путь» к пустому запросу (успешное вычисление) в наименьшей модели MP , намнужно ввести в множестве основных атомов MP какие-нибудьориентиры (систему координат), руководствуясь которымиможно вывести из запроса G0 пустой запрос .Например, так:$'MP?C0tt&%ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЧтобы запрос G0 =?C0 мог «отыскать путь» к пустому запросу (успешное вычисление) в наименьшей модели MP , намнужно ввести в множестве основных атомов MP какие-нибудьориентиры (систему координат), руководствуясь которымиможно вывести из запроса G0 пустой запрос .Или так:$'MP'$Mnrrr?C0'M2'M1M0&&&&$$%%%%ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯДля создания такой «системы слоев» в наименьшей моделиMP воспользуемся оператором непосредственного следования .ОпределениеПусть задана хорновская логическая программа P, состоящаяиз программных утверждений D1 , D2 , .
. . , DN .Оператором непосредственного следования TP для программыP называется отображениеTP : 2BP → 2BP ,удовлетворяющее следующему соотношению:для любой эрбрановской интерпретации I , I ⊆ BP , имеет месторавенствоTP (I ) = {A0 : D = A0 ← A1 , . . . , Ak ∈ [P], {A1 , . . . , Ak } ⊆ I }.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюBP — эрбрановский базис программы P, т. е.
множество всехосновных атомов программы.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюBP — эрбрановский базис программы P, т. е. множество всехосновных атомов программы.Таким образом, каждое подмножество I , I ⊆ BP — этоэрбрановская интерпретация, в которой истиннымиобъявляются те и только те атомы, которые содержатся вмножестве I .ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюВ математике (теории множеств) для каждого множества Mзапись 2M обозначает совокупность всех возможныхподмножеств множества M, включая само множество M ипустое множество ∅.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюВ математике (теории множеств) для каждого множества Mзапись 2M обозначает совокупность всех возможныхподмножеств множества M, включая само множество M ипустое множество ∅.Таким образом, 2BP — это множество всех эрбрановскихинтерпретаций программы P,ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюВ математике (теории множеств) для каждого множества Mзапись 2M обозначает совокупность всех возможныхподмножеств множества M, включая само множество M ипустое множество ∅.Таким образом, 2BP — это множество всех эрбрановскихинтерпретаций программы P,и оператор непосредственного следования TP : 2BP → 2BPпреобразует одни эрбрановские интерпретации программы P вдругие эрбрановские интерпретации.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюКак же проводится это преобразование интерпретаций?ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюКак же проводится это преобразование интерпретаций?[P] — это множество всех основных примеров программныхутверждений (правил и фактов) программы P,ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюКак же проводится это преобразование интерпретаций?[P] — это множество всех основных примеров программныхутверждений (правил и фактов) программы P,и каждое утверждение D = A0 ← A1 , A2 , .
. . , Ak понимается каквысказывание «если A1 и A2 и . . . и Ak , то A0 ».ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюКак же проводится это преобразование интерпретаций?[P] — это множество всех основных примеров программныхутверждений (правил и фактов) программы P,и каждое утверждение D = A0 ← A1 , A2 , . . .
, Ak понимается каквысказывание «если A1 и A2 и . . . и Ak , то A0 ».Таким образом,TP (I ) = {A0 : D = A0 ← A1 , . . . , Ak ∈ [P], {A1 , . . . , Ak } ⊆ I }.— это совокупность всех тех основных атомов A0 , которыеявляются непосредственными следствиями истинных винтерпретации I утверждений A1 , . .
. , Ak на основании правили фактов программы P.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПояснения к определениюЗначит, оператор TP : 2BP → 2BP , определяемыйсоотношениемTP (I ) = {A0 : D = A0 ← A1 , . . . , Ak ∈ [P], {A1 , . . . , Ak } ⊆ I },вычисляет для каждой эрбрановской интерпретации I новуюинтерпретацию TP (I ), состоящую из всех тех атомов, которыеявляются непосредственными следствиями, извлекаемыми изинтерпретации I при помощи фактов и правил программы P.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 1.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 1.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.Если I = ∅, то TP (I ) = ∅.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 1.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.Если I = ∅, то TP (I ) = ∅.Действительно, для любого основного терма t имеем P(t) ∈/ I,и это означает, что правило P(f (x)) ← P(x) не даетнепосредственных следствий из интерпретации I .ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 2.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.Если I = BP , то TP (I ) = BP \ {P(c)}.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 2.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.Если I = BP , то TP (I ) = BP \ {P(c)}.Действительно, коль скоро в интерпретации I истинновсе-все-все, то непосредственными следствиями интерпретацииI по правилу программы P будут все атомы вида P(f (t)).ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 2.Пусть задана хорновская логическая программаP : P(f (X )) ← P(X ),сигнатуры σ = hConst = {c}, Func = {f }, Pred = {P}i,состоящая из одного-единственного программногоутверждения.Если I = BP , то TP (I ) = BP \ {P(c)}.Действительно, коль скоро в интерпретации I истинновсе-все-все, то непосредственными следствиями интерпретацииI по правилу программы P будут все атомы вида P(f (t)).Однако программа P не позволяет получить атом P(c) вкачестве непосредственного следствия интерпретации I .ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ТогдаTP (∅) = {R(a), P(c)} (факты любой программы не требуютникаких предпосылок, и поэтому являются непосредственнымиследствиями любой интерпретации)ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ТогдаTP (∅) = {R(a), P(c)}TP2 (∅) = TP (TP (∅)) = {R(a), P(c), P(a)}(факты (3) и (4) попрежнему являются непосредственными следствиямиинтерпретации TP (∅), но теперь кроме них еще однологическое следствие можно получить по правилу (1))ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ТогдаTP (∅) = {R(a), P(c)}TP2 (∅) = TP (TP (∅)) = {R(a), P(c), P(a)}TP3 (∅) = {R(a), P(c), P(a), R(b)}(а теперь по правилу (2)добавляется еще одно непосредственное следование)ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ТогдаTP (∅) = {R(a), P(c)}TP2 (∅) = TP (TP (∅)) = {R(a), P(c), P(a)}TP3 (∅) = {R(a), P(c), P(a), R(b)}TP4 (∅) = {R(a), P(c), P(a), R(b), P(b)}(и вновь по правилу (2)добавляется еще одно непосредственное следование)ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯПример 3.Пусть задана хорновская логическая программаP : P(X ) ← R(X ), P(c);R(b) ← P(a);R(a) ←;P(c) ←;(1)(2)(3)(4)ТогдаTP (∅) = {R(a), P(c)}TP2 (∅) = TP (TP (∅)) = {R(a), P(c), P(a)}TP3 (∅) = {R(a), P(c), P(a), R(b)}TP4 (∅) = {R(a), P(c), P(a), R(b), P(b)}TP5 (∅) = TP4 (∅), и вообще TPn (∅) = TP4 (∅) при любых n ≥ 5.ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯОператор непосредственного следования TP обладает рядомполезных свойств.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
