Лекции В.А. Захарова (1157993), страница 13

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

Текст из файла (страница 13)

1. Завершаемость алгоритма.Вспомогательная лемма.В множестве троек натуральных чисел не существуетбесконечно убывающей последовательностиhk1 , m1 , n1 i  hk2 , m2 , n2 i  · · ·  hki , mi , ni i  hki+1 , mi+1 , ni+1 i  . . .Доказательство вспомогательной леммы.Самостоятельно.АЛГОРИТМ УНИФИКАЦИИИдея доказательства вспомогательной леммы.Предположим, что у Вас есть 1 000 000 руб. в произвольныхкупюрах.

Сыграем в игру. Правила игры таковы.1. Вы даете мне денежную купюру и взамен получаете правопотребовать от меня любую сумму в купюрах меньшегодостоинства.2. Если Вы вручаете мне купюру наименьшего достоинства,то взамен не получаете ничего.Докажите, что игра всегда будет оканчиваться тем, что Выостаетесь без денег.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т.

е.(i)E 0 −→ E 00 ⇒ H(E 0 )  H(E 00 ),где i = 1, 3, 4, 5.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 )  H(E 00 ),где i = 1, 3, 4, 5.Правило (1) ...f (t1 , . . . , tn ) = f (s1 , . . . , sn )E0 :......t1 = s 1(1)...−→ E 00 :t = s1 1...h1 (E 0 ) h1 (E 00 ), h2 (E 0 )  h2 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т.

е.(i)E 0 −→ E 00 ⇒ H(E 0 )  H(E 00 ),Правило (3) ...0s=xE :...где i = 1, 3, 4, 5. ...(3)00x =s−→ E :...h1 (E 0 ) h1 (E 00 ), h2 (E 0 )  h2 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 )  H(E 00 ),Правило (4) ...0s=sE :...где i = 1, 3, 4, 5. ...(4)00...−→ E :...h1 (E 0 ) h1 (E 00 ), h2 (E 0 ) h2 (E 00 ), h3 (E 0 )  h3 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 )  H(E 00 ),Правило (5)t1 = s 1 ...x = sjE0 :...tn = s nгде i = 1, 3, 4, 5.t1 {x/sj } = s1 {x/sj }...(5)x = sj−→ E 00 :...tn {x/sj } = sn {x/sj }h1 (E 0 )  h1 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство.

1. Завершаемость алгоритма.Значит, правила (1), (3, (4), (5) не могут применятьсябесконечно долго.Значит, рано или поздно либо будет применено одно из правил(2), (6), либо будет получена система, к которой неприменимони одно правило. В любом случае работа алгоритмаунификации завершится.АЛГОРИТМ УНИФИКАЦИИДоказательство.

2. Корректность алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)получается система уравнений, равносильная исходной, т. е.(i)E 0 −→ E 00 ⇒ E 0 ' E 00 ,где i = 1, 3, 4, 5.Это, очевидно, верно для правил (1), (3, (4) (убедитесь сами ).Покажем, что правило (5) также приводит к равносильнойсистеме.t1 = s 1t1 {x/sj } = s1 {x/sj } ... ...(5)x = sjx = sjE0 :−→ E 00 :......tn = s ntn {x/sj } = sn {x/sj }АЛГОРИТМ УНИФИКАЦИИДоказательство. 2. Корректность алгоритма.Предположим,что θ — унификатор системы уравнений E 0 , т.

е.t1 θ ≡ s 1 θ ...xθ ≡ sj θ...tn θ ≡ s n θТ. к. xθ ≡ sj θ, x ∈/ Varsj , согласно лемме о связке θ = {x/sj }θ.Следовательно,t1 {x/sj }θ ≡ s1 {x/sj }θ ...xθ ≡ sj θ...tn {x/sj }θ ≡ sn {x/sj }θЗначит, θ — унификатор системы уравнений E 00 . Аналогичнодоказывается, что всякий унификатор системы E 00 являетсяунификатором системы E 0 .АЛГОРИТМ УНИФИКАЦИИДоказательство.

3. Полнота алгоритма унификации.Как мы показали, рано или поздно при работе алгоритма либобудет применено одно из правил (2), (6), либо будет полученасистема, к которой неприменимо ни одно правило.Если к системе применяется правило (2), то в системе естьуравнение f (s1 , . . . , sn ) = g (t1 , . . . , tm ), f 6= g . Очевидно, длялюбой подстановки θ верно f (s1 , . . . , sn )θ 6≡ g (t1 , .

. . , tm )θ.Значит, система, содержащая такое уравнение,неунифицируема.Если к системе применяется правило (6), то в системе естьуравнение x = s, x ∈ Vars . Согласно лемме о связке для любойподстановки θ верно xθ 6≡ sθ. Значит, система, содержащаятакое уравнение, неунифицируема.Значит, выдача сообщения СТОП: НЕТ УНИФИКАТОРАозначает, что система неунифицируема.АЛГОРИТМ УНИФИКАЦИИДоказательство. 3. Полнота алгоритма унификации.Если к системе уравнений неприменимо ни одно правило, тоIв левых частях уравнений содержатся только переменные(иначе применимы правила (1), (2) или (3));Iни одна переменная из левой части больше нигде несодержится (иначе применимы правила (4), (5) или (6)).Значит, построенная система уравнений является приведеннойи имеет унификатор, который вычисляется по лемме оприведенной системе .КОНЕЦ ЛЕКЦИИ 8.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

ЗахаровЛекция 9.Резолютивный вывод.Корректность резолютивноговывода.Применение метода резолюций.РЕЗОЛЮТИВНЫЙ ВЫВОДО терминологии.Пусть задано выражение E и подстановка θ.Подстановка θ : Var → Var называется переименованием ,если θ — биекция.Выражение E θ называется примером выражения E .Если VarE θ = ∅, то пример E θ называется основным примеромвыражения E .Если θ — переименование, то пример E θ называется вариантомвыражения E .РЕЗОЛЮТИВНЫЙ ВЫВОДПримерПусть E = P(x, f (y )) ∨ ¬R(y , c).θ = {x/u, y /z, u/x, z/y } — переименование.E 0 = E {x/g (d), y /z} = P(g (d), f (z)) ∨ ¬R(z, c) — пример E .E 00 = E {x/g (d), y /c} = P(g (d), f (c)) ∨ ¬R(c, c) — основнойпример E .E 000 = E {x/u, y /z} = P(u, f (z)) ∨ ¬R(z, c) — вариант E .В частности, пустая (тождественная) подстановка являетсяпереименованием.РЕЗОЛЮТИВНЫЙ ВЫВОДПравило резолюции.Пусть D1 = D10 ∨ L1 и D2 = D20 ∨ ¬L2 — два дизъюнкта.Пусть θ ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D10 ∨ D20 )θ называется резольвентойдизъюнктов D1 и D2 .Пара литер L1 и ¬L2 называется контрарной парой .Правило резолюцииD10 ∨ L1 , D20 ∨ ¬L2,(D10 ∨ D20 )θθ ∈ НОУ(L1 , L2 )РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))D2 = Q(x) ∨ R(y , x) ∨ ¬P(g (z, y ), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z)){z}|D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z){z}|D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))|{z}D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z)){z}|D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z)x = g (z, y )E0 :f (y ) = zРЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z)){z}|D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z)(3),(5)x = g (z, y )x = g (f (y ), y )E0 :−→ E1 :f (y ) = zz = f (y )РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z)){z}|D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z) = θ = {x/g (f (y ), y ), z/f (y )}(3),(5)x = g (z, y )x = g (f (y ), y )E0 :−→ E1 :f (y ) = zz = f (y )РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))|{z}D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z) = θ = {x/g (f (y ), y ), z/f (y )}РезольвентаD0 = ¬R(g (x, z), f (z)) ∨ Q(x) ∨ R(y , x) θ|{z} |{z}D10D20РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))|{z}D10D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)|{z}D20Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)НОУ P(x, f (y )), P(g (z, y ), z) = θ = {x/g (f (y ), y ), z/f (y )}РезольвентаD0 = ¬R(g (g (f (y ),y ),y ),f (f (y )))∨Q(g (f (y ),y ))∨R(y, g (f (y ),y )).РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z){z}| {z }|D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x)g (x, z) = yE0 :f (z) = xРЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x)(3),(5)g (x, z) = yy = g (f (z), z)E0 :−→ E1 :f (z) = xx = f (z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x) = η = {x/f (z), y /g (f (z), z)}(3),(5)g (x, z) = yy = g (f (z), z)E0 :−→ E1 :f (z) = xx = f (z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x) = η = {x/f (z), y /g (f (z), z)}РезольвентаD0 = P(x, f (y )) ∨ Q(x) ∨ ¬P(g (z, y ), z) η| {z } |{z}D100D200РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z))| {z }D10D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z)| {z }|{z}D20D20Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)НОУ R(g (x, z), f (z)), R(y , x) = η = {x/f (z), y /g (f (z), z)}РезольвентаD0 = P(f (z),f (g (f (z), z)))∨Q(f (z))∨¬P(g (z,g (f (z), z)), z).РЕЗОЛЮТИВНЫЙ ВЫВОДПравило склейки.Пусть D1 = D10 ∨ L1 ∨ L2 — дизъюнкт.Пусть η ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D10 ∨ L1 )η называется склейкойдизъюнкта D1 .Пара литер L1 и L2 называется склеиваемой парой .Правило склейкиD10 ∨ L1 ∨ L2,(D10 ∨ L1 )ηη ∈ НОУ(L1 , L2 )РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨ ¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z) y =xz = f (c)E0 :f (x) = zРЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z) y =x y =c(1),(3),(5)z = f (c)z = f (c)E0 :−→ E1 :f (x) = zx =cРЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z) = η = {x/c, y /c, z/f (c)} y =x y =c(1),(3),(5)z = f (c)z = f (c)E0 :−→ E1 :f (x) = zx =cРЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z) = η = {x/c, y /c, z/f (c)}СклейкаD0 = P(x) ∨¬R(y , z, f (x)) η| {z }D10РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z)| {z }D10Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)НОУ R(y , z, f (x)), R(x, f (c), z) = η = {x/c, y /c, z/f (c)}СклейкаD0 = P(c) ∨ R(c, f (c), f (c)).РЕЗОЛЮТИВНЫЙ ВЫВОДОпределение резолютивного вывода.Пусть S = {D1 , D2 , .

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

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