Ещё одни лекции В.А. Захарова, страница 12
Описание файла
PDF-файл из архива "Ещё одни лекции В.А. Захарова", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 12 страницы из PDF
алгоритм унификации Мартелли-Монтанари всегдазавершает работу;2. если система уравнений E унифицируема , то в результатеработы алгоритма унификации будет построенаприведенная система уравнений, равносильная исходнойсистеме E;3. если система уравнений E неунифицируема , то врезультате работы алгоритма унификации будет выданосообщение СТОП: НЕТ УНИФИКАТОРА.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Уравнение x = t, где x ∈ Var , x ∈/ Vart , будем называтьприведенным уравнением системы E , если переменная x несодержится ни в каких других уравнениях системы E.Переменную x в этом случае будем называть приведеннойпеременной системы EКаждой системе уравнений E сопоставим характеристикуH(E) = h1 (E), h2 (E), h3 (E), — упорядоченную тройкунатуральных чисел, в которой1.
h1 (E) — общее число неприведенных переменных,содержащихся в системе E;2. h2 (E) — общее число функц. символов и констант,содержащихся в левых частях уравнений системы E;3. h3 (E) — общее число уравнений в системе E.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.
Завершаемость алгоритма.На множестве упорядоченных троек натуральных чисел введемотношение лексикографического порядка :M1 , M2 , M3 N1 , N2 , N3 N 1 < M1или N1 = M1 и N2 < M2или N1 = M1 , N2 = M2 и N3 < M3 .Пример.2, 11, 2 2, 10, 5578 1, 1001, 78АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Вспомогательная лемма.В множестве троек натуральных чисел не существуетбесконечно убывающей последовательностиk1 , m1 , n1 k2 , m2 , n2 · · · ki , mi , ni ki+1 , mi+1 , ni+1 .
. .Доказательство вспомогательной леммы.Самостоятельно.АЛГОРИТМ УНИФИКАЦИИИдея доказательства вспомогательной леммы.Предположим, что у Вас есть 1 000 000 руб. в произвольныхкупюрах. Сыграем в игру. Правила игры таковы.1. Вы даете мне денежную купюру и взамен получаете правопотребовать от меня любую сумму в купюрах меньшегодостоинства.2.
Если Вы вручаете мне купюру наименьшего достоинства,то взамен не получаете ничего.Докажите, что игра всегда будет оканчиваться тем, что Выостаетесь без денег.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E −→ E ⇒ H(E ) H(E ),где i = 1, 3, 4, 5.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.
Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E −→ E ⇒ H(E ) H(E ),Правило (1)⎧⎨ ...f (t1 , . . . , tn ) = f (s1 , . . . , sn )E :⎩...где i = 1, 3, 4, 5.⎧...⎪⎪⎪⎪t1 = s 1⎨(1)...−→ E :⎪⎪t = s1⎪⎪⎩ 1...h1 (E ) h1 (E ), h2 (E ) h2 (E )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т.
е.(i)E −→ E ⇒ H(E ) H(E ),Правило⎧ (3)⎨ ...s=xE :⎩...где i = 1, 3, 4, 5.⎧⎨ ...(3)x =s−→ E :⎩...h1 (E ) h1 (E ), h2 (E ) h2 (E )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E −→ E ⇒ H(E ) H(E ),Правило⎧ (4)⎨ ...s=sE :⎩...где i = 1, 3, 4, 5.⎧⎨ ...(4)...−→ E :⎩...h1 (E ) h1 (E ), h2 (E ) h2 (E ), h3 (E ) h3 (E )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.
Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E −→ E ⇒ H(E ) H(E ),Правило⎧ (5)t1 = s 1⎪⎪⎪⎪⎨ ...x = sjE :⎪⎪...⎪⎪⎩tn = s nгде i = 1, 3, 4, 5.⎧t1 {x/sj } = s1 {x/sj }⎪⎪⎪⎪...⎨(5)x = sj−→ E :⎪⎪...⎪⎪⎩tn {x/sj } = sn {x/sj }h1 (E ) h1 (E )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Значит, правила (1), (3, (4), (5) не могут применятьсябесконечно долго.Значит, рано или поздно либо будет применено одно из правил(2), (6), либо будет получена система, к которой неприменимони одно правило. В любом случае работа алгоритмаунификации завершится.АЛГОРИТМ УНИФИКАЦИИДоказательство.
2. Корректность алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)получается система уравнений, равносильная исходной, т. е.(i)E −→ E ⇒ E E ,где i = 1, 3, 4, 5.Это, очевидно, верно для правил (1), (3, (4) (убедитесь сами ).Покажем, что правило (5) также приводит к равносильнойсистеме.⎧⎧t1 = s 1t1 {x/sj } = s1 {x/sj }⎪⎪⎪⎪⎪⎪⎪⎪⎨ ...⎨ ...(5)x = sjx = sj−→ E :E :⎪⎪⎪⎪......⎪⎪⎪⎪⎩⎩tn = s ntn {x/sj } = sn {x/sj }АЛГОРИТМ УНИФИКАЦИИДоказательство. 2. Корректность алгоритма.Предположим, что θ — унификатор системы уравнений E , т. е.⎧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 . Аналогичнодоказывается, что всякий унификатор системы E являетсяунификатором системы E .АЛГОРИТМ УНИФИКАЦИИДоказательство.
3. Полнота алгоритма унификации.Как мы показали, рано или поздно при работе алгоритма либобудет применено одно из правил (2), (6), либо будет полученасистема, к которой неприменимо ни одно правило.Если к системе применяется правило (2), то в системе естьуравнение f (s1 , . . . , sn ) = g (t1 , . .
. , tm ), f = g . Очевидно, длялюбой подстановки θ верно f (s1 , . . . , sn )θ ≡ g (t1 , . . . , tm )θ.Значит, система, содержащая такое уравнение,неунифицируема.Если к системе применяется правило (6), то в системе естьуравнение x = s, x ∈ Vars . Согласно лемме о связке для любойподстановки θ верно xθ ≡ sθ. Значит, система, содержащаятакое уравнение, неунифицируема.Значит, выдача сообщения СТОП: НЕТ УНИФИКАТОРАозначает, что система неунифицируема.АЛГОРИТМ УНИФИКАЦИИДоказательство. 3. Полнота алгоритма унификации.Если к системе уравнений неприменимо ни одно правило, тов левых частях уравнений содержатся только переменные(иначе применимы правила (1), (2) или (3));ни одна переменная из левой части больше нигде несодержится (иначе применимы правила (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 = E {x/g (d), y /z} = P(g (d), f (z)) ∨ ¬R(z, c) — пример E .E = E {x/g (d), y /c} = P(g (d), f (c)) ∨ ¬R(c, c) — основнойпример E .E = E {x/u, y /z} = P(u, f (z)) ∨ ¬R(z, c) — вариант E .В частности, пустая (тождественная) подстановка являетсяпереименованием.РЕЗОЛЮТИВНЫЙ ВЫВОДПравило резолюции.Пусть D1 = D1 ∨ L1 и D2 = D2 ∨ ¬L2 — два дизъюнкта.Пусть θ ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D1 ∨ D2 )θ называется резольвентойдизъюнктов D1 и D2 .Пара литер L1 и ¬L2 называется контрарной парой .Правило резолюцииD1 ∨ L1 , D2 ∨ ¬L2,(D1 ∨ D2 )θθ ∈ НОУ(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))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара P(x, f (y )), ¬P(g (z, y ), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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) θ D1D2РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨ ¬R(g (x, z), f (z))D1D2 = Q(x) ∨ R(y , x) ∨¬P(g (z, y ), z)D2Возможная контрарная пара 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)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬R(g (x, z), f (z)), R(y , x)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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) η D1D2РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила резолюции.D1 = P(x, f (y )) ∨¬R(g (x, z), f (z)) D1D2 = Q(x) ∨R(y , x) ∨ ¬P(g (z, y ), z) D2D2Другая контрарная пара ¬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 = D1 ∨ L1 ∨ L2 — дизъюнкт.Пусть η ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D1 ∨ L1 )η называется склейкойдизъюнкта D1 .Пара литер L1 и L2 называется склеиваемой парой .Правило склейкиD1 ∨ L1 ∨ L2,(D1 ∨ 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) D1Возможная склеиваемая пара ¬R(y , z, f (x)), ¬R(x, f (c), z)РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z) D1Возможная склеиваемая пара ¬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) D1Возможная склеиваемая пара ¬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) D1Возможная склеиваемая пара ¬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) D1Возможная склеиваемая пара ¬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) D1Возможная склеиваемая пара ¬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)) η D1РЕЗОЛЮТИВНЫЙ ВЫВОДПример применения правила склейки.D1 = P(x) ∨¬R(y , z, f (x)) ∨ ¬R(x, f (c), z) D1Возможная склеиваемая пара ¬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 , .