Табличный FAQ (1109986)

Опр

Терм

Сложное (составное) преобразование

1. X isin Var => X - терм

2. С isin Const => С - терм

3. F isin Func, t1..tn - термы => F(t..) - терм

4. Других термов нет

Мн-во термов - Term

Опр

Var t

let t isin Term => Var t = {x:s isin Var, x вход. в t}

Опр

Формула

1. P isin Pred, t… isin Term => P(m)(t1,…,tm) - атом

2. ф, п, - формулы => ф * п – формула

3. ф - формула, x isin Var => (Q x ф) - формула (Q - квантор)

4. Других формул нет

Опр

Связанная переменная

Все вхождения x в область действия квантора - связанные. Если не связанная => свободная

Опр

Var ф

let ф isin Form => Var ф - множ-во свободных переменных ф

Опр

Замкнутая формула

let ф isin Form : Var ф = 0 => ф - замкнутая формула

Опр

Интерпретация (1го порядка)

I = (Di, Const', Func', Pred')

Di - предметная область ~= 0

Const' : Const -> Di

Func' : Func -> (D* -> D)

Pred' : Pred -> (D* -> {true, false})

Опр

Выполнимость в I

ф (x1…) - выполнима на I, если exists b1… : I |= ф[b1…]

Опр

Истинность в I

ф (x1…) - истинна на I, если all b1… : I |= ф[b1…]

Опр

Выполнимость

ф - выполнима, если exists I : ф выполнима в I

Опр

Противоречивость

ф - противоречива, если all I : ф не выполнима в I

Опр

Общезначимость

ф - общезначима, если all I : ф истинна в I. Обозн. - |= ф

Опр

Модель для множ-ва формул

let Г = {ф1...} - конечное или бесконечное множ-во замкнутых формул. I - модель для множ-ва формул Г, если all фi isin Г : I |= фi

Опр

Логическое следствие

let ф0 - замкнутая формула => ф0 - логическое следствие мн-ва формул Г, если all I : I - модель для Г => I |= ф0. Обозн. - Г |= ф0

Теор

О логическом следствии

let Г - конечное мн-во замкнутых формул (ф1,…фn), ф0 - замкнутая формула =>

Г |= ф0 <=> |= (ф1&…фn) -> ф0

Теор

О трудности проверки общезначимости

1). существует формула фи – тождественно истинная в любой I, Di – конечная область интерпретации. 2). exists I`: I` |fi

Опр

Подстановка

Сигма : Var -> Term - подстановка. Область подстановки - мн-во тех переменных, которые преобразовались не сами в себя. Связанные переменные не подставляются!!!

Опр

Свободная для терма t

let ф isin Form, x isin Var ф, t isin Term => x - свободная для терма T, если никакое свободное вхождение x в ф не лежит в области действия никакого квантора, связывающего переменные терма t

Опр

Таблица

Пара множеств <Г | Д>, Г, Д isin Form. Г - множество предполагаемо истинных формул, Д - множество предполагаемо ложных формул

Опр

Выполнимость таблицы

<Г, Д> - выполнима на I <=> exists b1…bn isin Di:

{all ф isin Г I |= ф,

{all ф isin Д I | ф

Опр

Табличный вывод

Пусть есть таблица T0, тогда табличный вывод - корневое дерево,

1) каждая вершина которого помечена таблицей

2) корень помечен T0

3) см. правила - м. б. Раздвоение

4) вершина висячая <=> T = <Г | Д> Г inter Д ~= 0, либо T = <Г | Д> Г, Д - Atom

Опр

Аксиома, закрытие

T = <Г | Д> Г inter Д ~= 0

Опр

Успешный вывод, опровержение

D - успешный вывод (опровержение), если D - конечное дерево и все висячие вершины D - аксиомы

Теор

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

Если таблица Tф, построенная для обоснования общезначимости формулы ф имеет успешный вывод, то ф - общезначима

Теор

Полноты

Если формула общезначима => существует успешный вывод для таблицы Tф

Опр

Процедура вывода

стр 25 матулекций

Сл1

|= ф <=> существует успешный табличный вывод для Tф

Сл2

Левенгейма-Скулема

Если ф выполнима, то существует интерпретация I, такая, что Di не более, чем счетно-бесконечная, I |= ф

Сл3

компактности

let Г - мн-во замкн формул => Г имеет модель <=> all конечное Г' isin Г : Г' имеет модель

Опр

равносильности

let ф, п isin Form. ф -= п <=> |= (ф->п) & (п->ф)

Опр

Подформула / замена

ф, п, х isin Form => ф[п] - п содержится в ф, как подформула. Ф [п / x] - ф-ла, полученная из ф заменой некоторых вхождений п на х

Теор

О равносильной замене

п,х,ф isin Form. Let |= п  x => |=ф[п]  ф[п/x]

Опр

Предваренная нормальная форма

Замкн формула F имеет пнф <=> F = Q1 x1 … M (X1…), Q - кванторы, М - не содержит кванторов и представима в КНФ

Теор

О существовании пнф

all ф - замкн exists пнф п: |= ф  п

Сл

let ф - замкн формула => exists пнф п: |=ф <=> |=п и ф - невып <=> п - невып

Опр

ССФ(Скулемовская стандартная форма)

ПНФ наз-ся ССФ if она имеет вид allx1allx2…allxn (D1&…&Dm)

Теор

о ССФ

Let фи-ПНФ, а фи'-ССФ, полученная из ССФ тогда фи выполнима <=> фи' выполнима

Утв

о Равносильности двух форм

Следующие 2 формы являются равносильными: |= allx (A&B) eq allx A & allx B

Опр

Противоречивость S(мн-во дизъюнктов)

S-противоречива, if all I exist <a1,…,an>in D(I,n) и exist Dj in S: I ~|= Dj[a1…an]

Утв

о Противоречивости

фи - ~|= <=> Sфи – противоречива

Опр

Эрбрановский Универсум

Пусть фи – формула. Пусть H0 = произвольная константа или множество констант формуты фи( если они есть). Тогда all i>=0: Hi+1 = Hi U { f(k)(t1,…,tk)}f(k) isin FUNC, t1,…,tk isin Hi } Тогда H = H0 U H1 U … - эрбрановский юниверсум – множество всех термов, которые можно построить из констант и функций данной формулы

Опр

H-интерпретация(эрбрановская)

Пусть фи – формула. Тогда Н-интерпретация ( эрбрановская ) – это < Hфи – эрбрановскйи юниверсум, c isin const fi, c isin Hfi, f(k) isin Func fi, в функциях значением каждого терма является он сам, P(k) isin Pred fi>

let p isin Pred, t1, …, tm isin H – термы без переменных, then P(m)(t1,…,tm) – основной атом

Bh – множество всех основных атомов – эрбрановский базис формулы – множество всех атомарных формул, которые можно построить из предикатов этой формулы и термов ее эрбрановского юниверсума

Теор

об эрбрановской интерпретации

Let имеется система дизъюнктов S. S - противоречива <=> S невыполнима ни в одной эрбрановской интерпретации

Опр

Семантическое дерево

Пусть Bn = {A1,A2,…} – H-базис Тогда семантическое дерево – (Ai)(узел)(~Ai) и так по всем слоям i

Опр

Основной пример дизъюнкт

Let имеется дизъюнкт D(x1,…,xn)=L1\/…\/Lk, D in S => основным примером D наз-ся дизъюнкт D', который получается в результате подстановки в D D'=D{x1/t1,…,xm/tm} основных термов t1,…,tm из H - эрбрановского универсума

Утв

об Основном примере дизъюнкта

Система дизъюнктов S-противоречива <=> all эрбрановской интерпретации I exist D in S: I |D', где D' - основной пример D

Утв

В тему

Пусть i = A₁^b1,…,a_n^bn – H-интерпретация, соотвю какой-то ветви семантического дерева, пусть d` = L`1\/…\/L`k – основной пример D isin S Тогда I |D`  {~L`1,…,~L`k}  I

Опр

Множество примеров дизъюнктов из S

Let S - система дизъюнктов => [S] - мн-во основных примеров дизъюнктов из S

Утв

В тему

S-противоречива<=> all эрбрановской интерпретации I exist осн. Пример D' in [S]: D'=L1'\/…\/Lk', {~L1',…,~Lk'}  I

Опр

Опровергающая дизъюнкт вершина

Let T - семантическое дерево Let v - вершина в T, Let из корня в вершину v идет путь L1,L2,…,L k=> Iv = {L1,L2,…,Lk}. Вершина v опровергает дизъюнкт D if exist D' - основной пример D: D' = L1'\/…\/Lk' и {~L1',…,~Lk'}  Iv

Опр

Опровергающий узел для S в T

v - опровергающий узел для S в T, if v - опровергает D, D in S и all u, лежащий между корнем и v в T не опровергает ни одного дизъюнкта из S

Лм

о семантическом дереве

If S - противоречива и T - произвольное семантическое дерево для S, то на каждой ветви T лежит опровергающий узел и число таких узлов конечно

Теор

Эрбрана

S - противореч <=> exist конечн. Подмножество S' in [S]: S' - противореч

Опр

Композиция подстановок

Пусть тета, эта – подстановки. Композиция подстановок ламбда = тета*эта: all x isin var ламбда(x) = ((х)эта)тета

Опр

Унификатор выражений

Подстановка Tta - унификатор выражений Е1 и Е2 <=> E1Tta = E2Tta

Опр

НОУ(наиболее общий унификатор)

Унификатор Eta выражений E1 и E2 называется НОУ if all унификатор Tta для Е1 и Е2 exist Ro in Subst: Tta = Eta.Ro

Опр

Унификатор для системы

Подстановка Tta: уравнения системы обращает в тождества

Опр

приведенная система

система термальных уравнений xi=ti наз-ся приведенной, если все х – переменные, все t –термы, множество переменных в левых частях не пересекается с множеством переменных в правых частях

Лм

о связке

Let x in Var, t in Term, Tta in Subst => Tta - унификатор x и t (xTta = tTta) <=> Tta={x/t}Tta

Утв

НОУ для приведенной системы

Для системы уравнений xi = ti НОУ = {xi/ti}

Опр

эквивалентность систем уравнений

2 какие-то ??? Системы уравнений (*) и (**) эквивалентны, if all Tta in Subst - унификатор первого <=> является унификатором второго

Опр

Алгоритм унификации Мартелло-Монтанари

Вход: { t1 = s1, …, tn = sn }

Procedure: while возможно do применять к списку равенств одно из 1-6 правил end_while

Выход: { x1 = t`1, …, xm = t`m } – приведунная система; { x1/t`1, …, xm/t`m } – НОУ

Правила: пусть ti = si – правило из списка

1). if ti = f( t`1, …, t`k), si = f( s`1, …, s`k ) then заменить равенство ti = si на к равенств t`k = s`k

2). если ti = f(T), si = g( S ), f  g then stop( не унифицир )

3). if ti = y isin var, si = x isin var, then удалить правило из списка

4). if si = x isin var, ti not isin var then заменить ti=si на si=ti

5). if ti = x isin var, si отличен от x и x isin хотябы одному уравнению списка, x not isin var si, then ко всем уравнениям tj = sj, j<>i, применить подстановку {x/si}

6). если ti = x isin var, si not isin var, x isin var si then stop( не унифицир )

Теор

алгоритм Мартелло-Монтанари

АММ 1)всегда останавливается 2)if исх система {t1=S1,…,tN=SN} унифицируема то АММ строит НОУ 3). Если исходная система не унифицируема, то Амм останавливается с ответом «не унифицир.»

Опр

Характеристика системы какой-то (*)

Характеристика системы (*) наз-ся тройка вида h = (альфа,бта,гма), где альфа-количество перем для которых нет ур-ния x=s , x~inVar si и x не встречается в других ур-ниях, бта - кол-во функцион символов в левых частях ур-ний, гма-общее кол-во ур-ий в системе

Утв

В тему

Этот порядок возрастания на N3 удовлетворяет условию обрыва убывающих цепей то есть ~exist бесконечно убывающей посл-ти троек

Опр

Переименование

Подстановка Tta={x1/y1,…,xn/yn}, где у1,…,yn попарно различны, наз-ся переименованием

Опр

Резольвента и склейка

Let D1,D2 - дизъюнкты 1) if D1=D1'\/L1, D2=D2'\/notL2, var D1 inter var D2 = 0, Let exists НОУ(L1,L2)=Tta => вариант D=(D1'\/D2')Tta, var D inter var D1 = 0, var D inter var D2 = 0, - резольвента D1, D2, L1 и ~L2 - контрарная пара 2) Let D1=D`1\/L1\/L2, НОУ(L1,L2) = h, then вариант D = ( D`1 \/ L1 )h, var D inter var D1 = 0, называется склейкой

Опр

Резолютивный вывод

Let S = {D1,…,Dn} - семейство дизъюнктов => резолютивным выводом из S наз-ся D1',…,Dn' - конечн посл-ть дизъюнктов такая что all I>=1 либо 1) Di – вариант Dj isin S либо 2) Di' - склейка Dj', j<i либо 3) Di' - резольвента Dj' и Dk', j,k < i

Об

Квадрат 

пустой дизъюнкт ( нет ни одной литеры, тождественная ложь )

Опр

Успешный вывод

Резолютивный вывод из S успешный (резолют опровержение )  D1',…,Dn' : Dn' = 

Теор

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

If из S резолютивно выводим дизъюнкт D то тогда S |= D ( |- R A => |= A )

Лм

о подъеме

Пусть D1, D2 – дизъюнкты, D`1, D`2 – основные примеры D1, D2; D`1 = D1Tta1, varD`1 = , D`2 = D2Tta2, varD`2 = , D`0 – резольвента D`1, D`2. Тогда exists D0 – резольвента D1, D2 и D`0 – основной пример D0.

Теор

о полноте для метода резолюций

Let S – система дизъюнктов => если S - противоречива то exists резолютивное опровержение S ( |= A => |- R A )

Опр

Концепция построения резолютивного вывода

Г |= exists x P(x) then |= Г -> exists x P(x) then not( Г -> exists x P(x) ) then all x ( Г & notP(x) ) then Г U { notP(x) } then в процессе резолютивного вывода notP(x){x/t}-> т.е. Г |= P(t)

Опр

Синтаксис логической программы

логическая_программа ::= список_программных_утверждений

список_прогр_утв ::= прогр_утв / прогр_утв; список_прогр_утв

прогр_утв ::= факт / процедура

факт :: = Атом <-

процедура ::= Атом <- тело_процедуры

тело_процедуры ::= Атом / Атомб тело_процедуры

Опр

Процедура,заголовок процедуры,тело процедуры

Конструкция вида A0 <- A1,…,An – процедура, A0 – заголовок процедуры, A1,…,An – тело процедуры

Опр

Запрос

G вида ?C1,C2,…,Cm – запрос ( цель, целевое утверждение ) или запрос ::= ?тело_процедуры

Опр

Хорновский дизъюнкт

Дизъюнкт, содержащий не более, чем одну положительную литеру, называется хорновским дизъюнктом. A1&A2&…&An->A0 – импликативная форма, ~A1\/…\/~An\/A0 – дизъюнктивная форма

Опр

Ответ на запрос

1). Tta = { x1/t1,…,xn/tn} – ответ на запрос G к P 2). Ответ Tta на запрос G к P – правильный, если P |= GTta

Опр

Модель программы

Если есть программа Р, то эрбрановская интерпретация I называется моделью дял Р если I |= P

Лм

о пересеч моделей

Let M1, M2 - модели логич пр-мы P => M0 = M1 inter M2 - модель пр-мы P

Теор

об основном правильном ответе или о главном свойстве наименьшей эрбрановской модели

Let P - логическая программа, А - атом, var A ={y1,…,yn}, Tta={y1/t1,…,yk/tk}, где t1,…,tk in Hp => Tta является прав ответом на запрос ?A <=> ATta isin Mp

Опр

Декларативная семантика

Let P - логич пр-ма H - интерпретация I – декларативная семантика для P; если all P(n) in Pred t1,…,tn  Hp, I |= P(n)[t1,…,tn]  P |= P(t1,…,tn)

Декларативная семантика – характеризация множества ответов программы

Теор

В тему

Let P - логическая программа(хорновская) => all P exists декларативная семантика I: I = Mp

Опр

Оператор непосредственного следования Tp

Пусть P – логическая программа, [P] – множество основных примеров программных утверждений, Bp – эрбрановский базис для Р, I  Bp. Оператором непосредственного следования для логической программы Р называется 1). Tp: 2^(Bp) -> 2^(Bp) (т.е. интерпретацию в интерпретацию) 2). all I  Bp Tp(I) = { A | A isin Atom, exists ( A <- A1,…,Am) isin [P], A1,…,Am isin I }

Утв

монотонность оператора непосредственного следования

Tp – монотонен т.е. если I1  I2 то Tp( I1 )  Tp( I2 )

Утв

I – модель для логической программы Р  Tp(I)  I

Опр

Неподвижная точка оператора Tp

I - H интерпретация наз-ся неподвижн точкой оператора Tp if Tp(I) = I

Опр

Наименьшая неподвижная точка оператора Tp

Let I isin fp(Tp) => I - неподвижная точка оператора Tp if all J isin fp(Tp) I  J

Теор

о наименьшей неподвижной точке

Пусть Р – (хорновская) логическая программа. Тогда 1), lfp(Tp) существует 2). lfp(Tp) = T_p⁰()\/T_p¹()\/T_p²()\/…, где T_pⁱ(I)=Tp(Tp(…i раз … (Tp(I)…)) 3). lfp(Tp) = Mp

Опр

Денотационная семантика

Денатационная семантика лог программы P - это интерпретация I: I isin lfp(Tp)

Теор

о денотационной семантике

Forall P - (хорновская) логической программы денотационная семантика exist, единственна и совпадает с декларативной семантикой

Опр

SLD резольвента

let G=?c1,…,ci-1, ci,…cm - целевое утверждение, P – хорновская логическая программа, D = A0 <- A1, …, An вариант программного утверждения из P, VarD ∩ VarG = Ø, θ = НОУ(ci, A0) => G' = ?(c1, …, ci-1,A1,…,An,ci+1, …, cm)θ называется SLD резольвента запроса G, обращенного к программе P с выделенной подцелью ci и активированным программным утверждением D с НОУ θ.

Опр

частичное SLD вычисление

let G0 - целевое утверждение, P - логическая программа => (G0,θ0)(G1,θ1)…(Gk,θk), такая, что all I =1,k-1 Gi+1 - SLD резольвента Gi - такая последовательность называется частичным SLD вычислением ответа на запрос G0 программы P

Опр

SLD вычисление

Частичное SLD вычисление ответа на запрос G в логической программе P называется SLD-вычислением, если выполнено следующее:

1) (G0,θ0)…(GN,θN)ڤ - вид частичного SLD-вычисления и результатом вычисления запроса (GN,θN) является пустой запрос - это успешное SLD-вычисление

2)имеет вид (G0,θ0),…,(GN,θN)■ и наз-ся законченным, если ни одно выделенное в запросе GN и ни одна активизация программного утверждения не применимы для получения SLD-резольвенты. Вычисление называется тупиковым.

3) (G0,θ0)…(GN,θN)... - бесконечное вычисление

Опр

Вычислимый ответ

let (G0,θ0),…,(Gn,θn)ڤ - успешное SLD вычисление ответа на запрос G0 к логической программе P, такое, что множество целевых переменных G0{y1,…,yk}. Тогда подстановка η = θ0...θN|y1…yk - проекция композиции подстановки θ0...θN на целевые переменные называется вычислимым ответом на G0 к P.

Опр

Операционная семантика логической программы

интерпретация I = succ P

Опр

Множество успехов логической программы

let P - логическая программа => Множеством успехов логической программы P называется SuccP = {A| A - осн. Атом, т.е. А isin Bp: ?A имеет SLD опровержение для P }

Теор

Корректность операционной семантики относительно декларативной

let θ - вычислимый ответ на G к P => θ - правильный ответ

Сл-ие

succ P <<= Mp

Опр

SLD квазивычисление

let G - запрос к логической программе P => SLD квазивычислением G к P называется последовательность пар (G0,η0),(G1,η1),…(Gk,ηk), где G0=G и для любого I>=0, I<k выполняется следующуе утверждение Gk=?c1,…,cj-1,cj,cj+1,…cn существует вариант D' = А0 <- A1,A2,...,Am isin P, ηk - унификатор ( не обязательно НОУ ) cj, A0, Gk+1 = ?(c1,…,cj-1,A1,A2,...,Am,cj+1,…cn)ηk

Лм

(О подъеме для SLD квазивычислений)

let G - запрос к логической программе P , θ isin Subst, предположим, что Gθ имеет успешное SLD квазивычисление, т.е. (G0,η0),(G1,η1),…(Gk,ηk)ڤ => G имеет успешное SLD-вычисление такое, что для вычисленного ответа λ найдется ρ isin Subst:λρ = θη0η1...ηk|y1...yn

Теор

(полноты относительно Succ)

SuccP >>= Mp all P

Теор

(полноты относительно вычислимых ответов)

let θ - правильный ответ на G к P => exists вычислимый ответ λ на G к P такой, что θ = λρ, ρ isin Subst

Опр

Построение Pтт по МТ

Для любой команды МТ вида qabq`R соответствует пара Conf( x.w, q, a.w` ) <- conf( b.w, q`, x.w` ); conf( w, q, a.nil ) <- conf( b.w, q`, a0.nil ). Для любой команды вида qabq`L соответствет пара conf( x.w, q, a.w` ) <- conf( w, q`, a"b".w` ); conf( nil, q, a.w` ) <- conf( nil, q`, a0.nil"b".w` )

Лм

Лемма 1

Пусть π - программа МТ, Pπ - логическая программа

α=(w',q,w'') β=(u',q*, u'')

Тогда α->β <=> ?Conf(k1((u')^(-1)), q* k1(u'')) является SLD-резольвентой по логической программе Pπ. Здесь (a)^(-1) - обращение цепочки a, К1 - конструктор списка

(то что может сделать МТ за один шаг, мы можем получить за один шаг резолютивного вывода)

Теор

Об универсальности логического программирования

Для all МТ π = <Q,K> exists логическая программа Pπ такая, что all начальной конфигурации α0 = (w',q1,w'') МТ имеет на α0 бесконечное вычисление <=> запрос ?Conf(k1((w')^(-1)), qo, k1(w'')) к P имеет единственное бесконечное SLD вычисление

МТ имеет на α0 конечное вычисление с результатом an = ( u`, q0, u`` ) <=> запрос ?conf( K1( (w` )^(-1) ) , q0, K1( w`` ) ) имеет единственное успешной SLD-вычисление, которое завершается ...->conf( K1((u`)^(-1)), q0, K1(u``))->ڤ

Теор

Геделя о неразрешимости проблемы общезначимости для классической логики предикатов

Не существует алгоритма решения проблемы общезначимости, т.е. Такого алгоритма A(φ) = {1, φ - общезнач

{0, φ - необщезнач

Опр

Правило вычисления

Правило вычисления R: G->AtomG т.е. Правило выбора Bk из Q = B1…Bn

Опр

SLD вычисление запроса G к логической программе P

SLD вычисление запроса G к логической программе P - это последовательность

(G0,θ0),(G1,θ1),…,(Gn,θn), где G0 = G и для каждого n Gn+1 - SLD резольвента G и некоторого выражения D' isin P, причем подцель C isin Gn выбирается по правилу R

Лм

переключательная

let G=?c1,…,cm - запрос к логической программе P, let G имеет некоторое успешное SLD-вычисление, которое представляется последовательностью пар (G0,θ0),(G1,θ1),…,(Gn,θn),ٱ

let q-й член этой последовательности (Gq,θq) имеет вид Gq = с1, … , сi, … cm, D=A0 <- A1,A2,...,Ak, НОУ( Ci, A0 ) = h1, Gq+1 = ?(C1,...,Ci-1,A1,...,Ak,...,Cm)h1, пусть на следующем шаге был получен Gq+2 вида ?( C1, ..., Ci-1, A1, ..., Ak, A`1,...A`l, ...,Cm)h1h2 где НОУ( Cj, A`0 ) = h2, D` = A`0 <- A`1,...,A`l. Тогда существует SLD-вычисление (успешное) G к P такое, что (G0,Л0)(G^1,Л1)...(G^n,Лn),ٱ отличающийся от предыдущего тем, что G^q = C1,...,Ci,...,Cj,...,Cm, D` = A`0 <- A`1,...,A`l, НОУ( Cj, A`0 ) = m1, G^q+1 = ?(C1,...,Ci,...,A`1,...,A`l,...,Cm)m1, D=A0 <- A1,A2,...,Ak, НОУ( Cim1, A0 ) = m2, G^q+2 имеет вид ?(C1,...,A1,...,Ak,...,A`1,...,A`l,...Cm)m1m2

Замечание: эта лемма говорит о том, что неважно, в каком порядке мы вычисляем ответы, мы получим ответы, отличающиеся друг от друга только переименованием

Теор

о независимости правила вычисления

let G – запрос к логической программе P, R1,R2 - 2 правила вычисления => запрос имеет успешное SLD-вычисление по правилу R1 с вычислимым ответом θ1 <=> запрос имеет успешное SLD-вычисление по правилу R2 с вычислимым ответом θ2 и при этом ответ θ1 =θ2ρ, где ρ – переименование

Теор

о сильной полноте SLD-вычислений)

let G – запрос к логической программе P, R - правило вычисления, let θ - правильный ответ на G к P => exists SLD-вычисление с правилом вычисления R с вычислимым ответом η: θ = ηρ, где ρ isin Subst

Опр

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

Во всех логических системах программирования каждый раз выбирается самая левая подцель ( all G :- R( G ) = 1 ). Это правило называется стандартным правилом вычисления.

Опр

дерево SLD-вычисления G к P по правилу R

let G - запрос к логической программе P, R - правило вычисления => деревом SLD-вычисления G к P по правилу R называется корневое дерево:

1. Корню дерева приписан исходный запрос

2. Если вершине V приписан запрос G':G''1,G''2,…G''k - всевозможные SLD-резольвенты, полученные из G`, обращен. к Р по правилу R с НОУ( 1, 2,…, k соответственно, то из V выходит k дуг, направленных в вершины U1, U2, …, Uk, которым приписаны G``, …, G``k, а дугам, ведущим в них, приписаны 1, 2,…, k.

Каждая ветвь представляет одно из SLD-вычислений G к P по правилу R, т.е. это дерево всевозможных SLD-вычислений G к P по R. Некоторые ветви могут быть успешными (ٱ), некоторые – тупиковыми (■), некоторые – бесконечными.

Опр

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

Стратегия вычисления логических программ - это алгоритм обхода дерева SLD-вычислений

Выделяются два способа: поиск в ширину и поиск в глубину

Св-во

Обработка cut

Как только появился запрос, содержащий !, мы помечаем его предшественника звездочкой *. Когда мы получим запрос, начинающийся с !, мы тоже помечаем его звездочкой *. “Альтернативные” ветви между звездочками не исследуются. При обходе дерева с возвратами мы, попав в нижнюю звездочку, откатываемся в верхнюю.

Опр

Интуиционистская интерпретация

P = { p1, p2, …} – множество элементарных высказываний

Form: 1). p isin P 2). not y, y&z, y\/z, y->z

J = < W, R, L >б где W = { w1, w2, … } – непустое множество возможных знаний,

R  W x W такое, что: 1). R – рефлексивно т.е. all w R(w,w) 2). R – транзитивно т.е. all w1, w2, w3: R( w1, w2 ) & R( w2, w3 ) -> R( w1, w3 ) 3). R – антисимметрично т.е. all w1, w2: R( w1, w2 ) & R( w2, w1 ) -> w1 = w2. Тогда R – отношение частичного порядка.

L: P x W -> { true, false } – оценка знаний, L( p, w ) = true, R( w, w` ) => L( p, w` ) =true

Отношение выполнимости:

I, w |= p, p isin P  L( p, w ) = true

I, w |= p&q  I,w |= p & I,w |=q

I, w |= p\/q  I,w |= p \/ I,w |=q

I, w |= p->q  forall w` isin W: ( R( w,w`), I, w` |= p => I,w` |= q )

I, w |= not y  forall w` ( R(w,w`) => I,w` |y )

В интуиционистской логике нарушаются некоторые законы классической логики ( P \/ not p = true, not not p = p ), неверны доказательства от противного (|(not p -> not not p)->p)

forall x y(x)  y( t1 ) /\ … /\ y( t n ) /\ …

exists x y(x)  y( t1 ) \/ … \/ y( t n ) \/ …

Утв

|(I)=y\/z

|(I)=y\/z  |(I)=y или |(I)=z

Сл-ие1

Г|(I)= y\/z  Г|(I)=y или Г|(I)=z

Сл-ие2

Экзистенциальное свойство

Г |(I)= exists x y(x)  для некоторого t isin Term Г |(I)=y(t)

Опр

интуиционистский закон

φ – интуиционистский закон (|(I)= φ) <=> all I – интуиционистской модели

all w isin W - в любом состоянии знаний I,w |(I)= φ

Опр

модальные логики

P = { p1, p2 ,… } – пропозициональные переменные

Form: 1). p, pisin P 2). not y, y /\ z, y\/ z, y -> z, y (модальность необходимого – всегда), y (модальность возможного - иногда)

Опр

модальная интерпретация

I = < W, R, L >, где

W = { w1, w2, … } – непустое множество альтернативных ( возможных ) миров

R  W x W – отношение достижимости ( перехода ). Если ( w`, w`` ) isin R то говорят, что w` видит w``.

L: P x W -> { true, false } – оценка высказываний

Опр

Отношение выполнимости в модальной логике

I,w |= y  y выполнима в I в мире w.

1). y = p => I,w |= y  L(y,w) = true

2). not y, y\/z, y/\z, y->z – также, как в классической логике

3). y = z: I,w |= y  forall w` if (w,w`) isin R then I,w` |= z

y = z: I,w |= y  exists w` isin W: if (w,w`) isin R then I,w` |= z

Опр

Прикладные темпоральные логики

Миры – это состояния. Есть отношение достижимости одного состояния из другого.

P = { p1, p2 ,… } – состояния, Form: 1). p, pisin P 2). not y, y /\ z, y\/ z, y -> z

Операторы: 1). X – сдвиг по времени – neXt time. Xy – y будет верно в момент времени, непосредственно следующий за настоящим 2). G – инвариантность – Globally. Gy – начиная со следующего момента времени y будет всегда верно 3). F – происшествие – Future. Fy – свойство y рано или поздно будет выполнено обязательно 4). U – до тех пор, пока – Until. yUz – y будет верно во всех последующих состояниях, пока не произойдет событие, выражающее свойство z. 5). R – сброс – Release. yRz – свойство z будет выполнено либо бесконечно долго, либо наступит момент, когда y будет верно.

Опр

Логика LTL – линейная темпоральная логика

P – пропозициональные переменные

not y, y\/z, y/\z, y->z, Xy, Gy, Fy, yUz, yRz – формулы

M = < S, R, L > - модель:

S не пусто, s isin S – состояния

R  SxS, R – отношение перехода (тотальное): forall s` isin S exists s`` isin S: (s`,s``) isin R ( т.е. система всегда может совершить шаг)

L: PxS -> { true, false } – оценка

Модель можно представлять как граф.

Опр

вычисление (трасса)

π = s1,s2,s3,… - вычисление (трасса) в М если all i>=1 (si,si-1) isin R

π |= φ - φ выполнима на трассе π

Обозн π[i]=si, π^(i) = si,si+1,…,sn,..

Опр

Отношение выполнимости в модели логики LTL

1). y = p isin P TT |= y  L( TT[1],p ) = true 2). not, /\, \/, -> аналогично классической логике 3). TT |= Xy  TT² |= y ( TT²=s2,s3,…) 4). TT |= Gy  forall i >= 1 TT^i |= y 5). TT |= Fy  exists i >= 1: TT^i |= y 6). TT |= yUz  exists i >= 1: TT^i |= z, all j isin [ 1, i ): TT^j |= y 7). TT |= yRz  all i>=1, all j isin [ 1, i ): if TT^j | y then TT^i |= z.

В модели М в состоянии s выполняется формула M,s |= y  all TT: TT[1] = s: TT |= y

Опр

Логика CTL – логика деревьев вычислений

В дополнение к множеству состояний и классическим логическим not, /\, \/, -> вводятся два комплекта темпоральных операторов: AX, AG, AF, AU, AR, EX, EG, EF, EU, ER, где A, E – аналоги кванторов по вычислениям ( по трассам ).

Опр

Отношение выполнимости модели логики CTL

Модель вводится аналогично логике LTL.

1). y = p isin P M,s |= y  L( p,s ) = true 2). not, /\, \/, -> аналогично классической логике 3). M,s |= AXy  all TT в модели М: TT[1] = s, TT |= Xy. Пусть @ isin { F, G }. M,s |= A@y  all TT в модели М: TT[1] = s, TT |= @y. Пусть * isin { U, R }. M,s |= yA*z  all TT в модели M: TT[1] = s, TT |= y*z. 4). M,s |= EXy  exists TT в модели М: TT[1] = s, TT |= Xy. Далее аналогично.

Опр

Отношение равносильности для формул логики CTL

yz  all M, all s isin S: M,s |= y => M,s |= z.

Некоторые равносильные формулы: AFy  not EG not y; EFy  true EUy; AGy  not EF not y  not( true EU not y )

Опр

Алгоритм model-checking

страница 112-114 матулекций