Теормин 2014 (avasite), страница 3

Пусть D1 = D₁’ ∨ L1 и D2 = D₂’ ∨ ¬L2 — два дизъюнкта. Пусть θ ∈ НОУ(L1, L2). Тогда дизъюнкт D₀ = (D₁’∨D₂’)θ называется резольвентой дизъюнктов D1 и D2.

Пара литер L1 и ¬L2 называется контрарной парой.

Правило резолюции , θ ∈ НОУ(L1, L2)

Правило склейки.

Пусть D1 = D₁’ ∨ L1 ∨ L2 — дизъюнкт. Пусть η ∈ НОУ(L1, L2).

Тогда дизъюнкт D0= (D₁’ ∨ L1)η называется склейкой дизъюнкта D1. Пара литер L1 и L2 называется склеиваемой парой.

Правило склейки , η ∈ НОУ(L1, L2)

Определение резолютивного вывода.

Пусть S = {D1, D2, …, DN} — система дизъюнктов. Резолютивным выводом из системы дизъюнктов S называется конечная последовательность дизъюнктов D1’, D2’, …, Di’, D_i+1’, …, Dn’, в которой для любого i, 1 ≤ i ≤ n, выполняется одно из трехусловий:

1. либо Di’ — вариант некоторого дизъюнкта из S

2. либо Di’ — резольвента дизъюнктов Dj’ и Dk’, где j , k < i

3. либо Di’ — склейка дизъюнкта Dj’, где j < i.

Дизъюнкты D1’, D2’, …, Dn’ считаются резолютивно выводимыми из системы S.

Резолютивный вывод называется успешным (или, подругому, резолютивным опровержением), если этот вывод оканчивается пустым дизъюнктом □.

Теорема корректности резолютивного вывода

Если из системы дизъюнктов S резолютивно выводим пустой дизъюнкт □, то S — противоречивая система дизъюнктов.

(следует из лемм, доказывающих, что склейка и резольвента являются логическими следствиями)

Лемма 1.

Если D0— резольвента дизъюнктов D1 и D2, то D1, D2|= D0

Лемма 2.

Если D0 — склейка дизъюнкта D, то D |= D₀.

Лекция 10. Полнота резолютивного вывода.

Теорема о полноте резолютивного вывода.

Если S – противоречивая система дизъюнктов, то из S резолютивно выводим пустой дизъюнкт □.

(По теореме Эрбрана можно свести противоречивую систему дизъюнктов к конечности, потом воспольземся леммой об основных примерах дизъюнктов, а потом перейдём от неё к самим дизъюнктам через лемму о подъёме)

Лемма об основных примерах дизъюнктов.

Если S’ – конечная противоречивая система основных примеров дизъюнктов, то из S’ резолютивно выводим пустой дизъюнкт □.

(По индукции по количеству различных основных атомов в системе. Базис – если нету атомов, а система противоречива, значит она – уже пустой дизъюнкт. Индуктивный переход – возьмём некоторый основной атом, разобьём все дизъюнкты на 3 множества, где этот атом встречается, встречается с отрицанием, и не встречается. Построим все возможные резольвенты и объединим это множество с 3-м упомянутым ранее, - докажем, что оно противоречиво. Возьмём любую интерпретацию, для определённости – наш атом в ней выполнен. Но система дизъюнктов не выполняется, а дальше разбираем варианты, что именно не выполняется в нашей интерпретации. В одном случае – ясно как делать, а во втором случае нужно построить вспомогательную интерпретацию, которая отличается от начальной лишь тем, что выбранный основной атом в ней не выполняется, и рассмотрим теперь все эти множества для новой интерпретации)

Лемма о подъёме.

Пусть D₁ и D₂ – два дизъюнкта, и при этом Var D₁ ∩ Var D₂ = ∅

Пусть D₁’=D₁θ и D₂’ =D₂θ – два основных примера этих дизъюнктов D₁ и D₂.

Пусть D₀’ – резольвента дизъюнктов D₁’ и D₂’.

Тогда из дизъюнктов D₁ и D₂ резолютивно выводим дизъюнкт D₀, основным примером которого является D₀’.

(Т.к. дизъюнкты не пересекаются, то подстановку можно разделить отдельно для каждого дизъюнкта, литера из контрарной пары имеет свои прообразы (могут быть разные и несколько), которые породили её в качестве части основного примера. Все указанные литеры (отдельно для каждого дизъюнкта) унифицируемы и у них есть НОУ – который является склейкой этих литер. Так же мы запомним тот унификатор, который приводит найденный НОУ к первоначальному, которые при объединении от обоих дизъюнктов дадут унификатор, а значит есть НОУ необходимый для применения резольвентного правила, причём для полученного резольвента основных примеров будет тоже являться примером)

Лекция 11. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.

Стратегия резолютивного вывода – вывод с дополнительными ограничениями на выбор подходящих пар дизъюнктов для получения резольвент.

Стратегия резолютивного вывода называется полной, если она позволяет вывести пустой дизъюнкт □ из любого противоречивого множества дизъюнктов.

Семантическая резолюция – резолюция с правилом I-резолюции – т.е. при построении резольвенты, оба дизъюнкта-предпосылки должны принадлежать разным множествам S₁’ и S₂’.

Теорема полноты I–резолюции

Если система дизъюнктов S противоречива, то для любой интерпретации I существует успешный I-резолютивный вывод пустого дизъюнкта □ из S .

Входная резолюция

Предположим, что в системе дизъюнктов S выделен некоторый дизъюнкт D₀.

Тогда резолютивный вывод пустого дизъюнкта □ из системы дизъюнктов S можно строить, руководствуясь следующими соглашениями:

1. Для построения первой резольвенты D₁ выбирается дизъюнкт D₀ и некоторый дизъюнкт D ∈ S\{D₀};

2. Для построения i-ой резольвенты D_i Выбирается резольвента D_i−1, построенная на предыдущем шаге вывода, и дизъюнкт D∈S.

Резолютивный вывод такого вида будем называть входным резолютивным выводом, инициированным дизъюнктом D₀.

Хорновские дизъюнкты – класс формул, для которых резолютивное опровержение всегда имеет линейную структуру.

Литера L называется положительной, если L — это атом.

Литера L называется отрицательной, если L = ¬A, где A — это атом.

Дизъюнкт D = L₁ ∨ L₂ ∨ … ∨L_n называется хорновским дизъюнктом (horn clause), если среди литер L₁, L₂, …, L_n имеется не более одной положительной литеры.

Логические программы. Резолютивное опровержение систем хорновских дизъюнктов — это вычисление ответов на простые запросы, обращенные к базе позитивных знаний. Базы позитивных знаний (хорновские дизъюнкты) становятся, таким образом, логическими программами.

КОЛЛОКВИУМ КОЛЛОКВИУМ КОЛЛОКВИУМ КОЛЛОКВИУМ КОЛЛОКВИУМ КОЛЛОКВИУМ КОЛЛОКВИУМ

Лекция 12. Хорновские логические программы синтаксис. Декларативная семантика логических программ.

Императивное программирование: программа — это автомат, описывающий последовательности операторов (команд).

Функциональное программирование: программа — это система уравнений, описывающая вычисляемую функцию.

Логическое программирование: программа — это множество формул, описывающих условия решаемой задачи.

Синтаксис логических программ:

«заголовок» ::= «атом»

«тело» ::= «атом» | «тело», «атом»

«правило» ::= «заголовок» ← «тело»;

«факт» ::= «заголовок»;

«утверждение» ::= «правило» | «факт»

«программа» ::= «пусто» | «утверждение» «программа»

«запрос» ::= □ | ? «тело»

Главная особенность логического программирования — полисемантичность: одна и та же логическая программа имеет две равноправные семантики, два смысла.

Программисту важно понимать, ЧТО вычисляет программа. Такое понимание программы называется декларативной семантикой программы.

Компьютеру важно «знать», КАК проводить вычисление программы. Такое понимание программы называется операционной семантикой программы.

Пусть P — логическая программа, D — программное утверждение, а θ — подстановка. Тогда

1. Dθ — пример программного утверждения D,

2. если θ — переименование, то Dθ — вариант программного утверждения D,

3. если VarDθ = ∅, то Dθ — основной пример программного утверждения D,

4. [D] — множество всех основных примеров программного утверждения D,

5. [P] — множество всех основных примеров всех утверждений программы P .

Пусть G =?C1, C2, …, Cm — запрос. Тогда

1. атомы C1, C2, …, Cm называются подцелями запроса G,

2. переменные множества называются целевыми переменными,

3. запрос □ называется пустым запросом,

4. запросы будем также называть целевыми утверждениями.

Логические программы и логические формулы

Каждому утверждению логической программы сопоставим логическую формулу:

1. Правило: D’ = A0 ← A1, A2, …, An

D’ = ∀X1…∀Xk (A1&A2& … &An → A0), где {X1, …, Xk} =

1. Факт: D’’ = A;

D’’ = ∀X1…∀Xk A, где {X1, …, Xk} = VarA

1. Запрос: G = ?C1, C2, …, Cm

G = C1&C2& . . . &Cm

Определение (правильного ответа)

Пусть P — логическая программа, G — запрос к P с множеством целевых переменных Y1, …, Yk.

Тогда всякая подстановка θ = {Y1/t1, …, Yk/tk} называется ответом на запрос G к программе P.

Ответ θ = {Y1/t1, …, Yk/tk} называется правильным ответом на запрос G к программе P, если P |= ∀Z1. . . ∀ZN Gθ, где {Z1, . . . , ZN} = .

Под операционной семантикой понимают правила построения вычислений программы. (Операционная семантика описывает, КАК достигается результат работы программы)

Определение SLD-резолюции (Linear resolution with Selection function for Definite clauses (Р. Ковальски))

Пусть

1. G = ? C1, …, Ci, …, Cm — целевое утверждение, в котором выделена подцель Ci,

2. D’= A₀’← A₁’, A₂’, …, A_n’ — вариант некоторого программного утверждения, в котором VarG ∩ VarD’ = ∅,

3. θ ∈ НОУ(Ci, A₀’) — наиб. общ. унификатор подцели Ci и заголовка программного утверждения A₀’.

Тогда запрос G’ = ?(C1, …, C_i−1, A₁’, A₂’, …, A_n’, C_i+1, …, Cm)θ

называется SLD-резольвентой программного утверждения D’ и запроса G с выделенной подцелью Ci и унификатором θ.

Определение SLD-резолютивного вычисления

Пусть

1. G0 = ?C1, C2, …, Cm — целевое утверждение,

2. P = {D1, D2, …, DN} — хорновская логическая программа.

Тогда (частичным) SLD-резолютивным вычислением, порожденным запросом G0 к логической программе P называется последовательность троек (конечная или бесконечная) (Dj1, θ1, G1), (Dj2, θ2, G2), …, (Djn, θn, Gn), …, в которой для любого i, i ≥ 1,

1. Dji ∈ P, θi ∈ Subst, Gi— целевое утверждение (запрос);

2. запрос Gi является SLD-резольвентой программного утверждения Dji и запроса G_i−1 с унификатором θi

Частичное SLD-резолютивное вычисление

comp = (Dj1, θ1, G1), (Dj2, θ2, G2), …, (Djk, θn, Gn) называется

1. успешным вычислением (SLD – резолютивным опровержением), если Gn = □;

2. бесконечным вычислением, если comp — это бесконечная последовательность;

3. тупиковым вычислением, если comp — это конечная последовательность, и при этом для выделенной подцели запроса Gn невозможно построить ни одной SLD-резольвенты.

Определение (SLD-резолютивного вычисления)

Пусть

1. G0 = ? C1, C2, …, Cm — целевое утверждение с целевыми переменными Y1, Y2, . . . , Yk,

2. P = {D1, D2, …, DN} — хорновская логическая программа,

3. comp = (Dj1, θ1, G1), (Dj2, θ2, G2), …, (Djn, θn, □) — успешное SLD-резолютивное вычисление, порожденное запросом G к программе P.

Тогда подстановка θ = (θ1 θ2 … θn)|_Y1,Y2,...,Yk, представляющая собой композицию всех вычисленных унификаторов θ1, θ2, …, θn, ограниченную целевыми переменными Y1, Y2, …, Yk, называется вычисленным ответом на запрос G0 к программе P.

Лекция 13. Корректность операционной семантики. Полнота операционной семантики.

Определение правильного ответа

Пусть P — логическая программа, G — запрос к P с множеством целевых переменных Y1, …, Yk. Тогда всякая подстановка θ = {Y1/t1, …., Yk/tk} называется ответом на запрос G к программе P. Ответ θ = {Y1/t1, …, Yk/tk} называется правильным ответом на запрос G к программе P, если P |= ∀Z1 …∀Z NGθ, где {Z1, …, ZN} =

Определение вычисленного ответа

Пусть

1. G0 = ? C1, C2, …, Cm — целевое утверждение с целевыми переменными Y1, Y2, …, Yk,

2. P = {D1, D2, …, DN} — хорновская логическая программа,

3. comp = (Dj1, θ1, G1), (Dj2, θ2, G2), …, (Djn, θn, □) — успешное SLD-резолютивное вычисление, порожденное запросом G к программе P.

Тогда подстановка θ = (θ1 θ2 … θn)| Y1,Y2,...,Yk, представляющая собой композицию всех вычисленных унификаторов θ1, θ2, …, θn, ограниченную целевыми переменными Y1, Y2, …, Yk, называется вычисленным ответом на запрос G0 к программе P.

Теорема (корректности операционной семантики)

Пусть

1. G0= ? C1, C2, …, Cm — целевое утверждение,

2. P = {D1, D2, …, DN} — хорновская логическая программа,

3. θ — вычисленный ответ на запрос G0 к программе P.

Тогда θ — правильный ответ на запрос G0 к программе P.