9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций (1158023)

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

Текст из файла

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 , .

. . , DN } — система дизъюнктов.Резолютивным выводом из системы дизъюнктов S называетсяконечная последовательность дизъюнктов0D10 , D20 , . . . , Di0 , Di+1, . . . , Dn0 ,в которой для любого i, 1 ≤ i ≤ n, выполняется одно из трехусловий:1. либо Di0 — вариант некоторого дизъюнкта из S;2. либо Di0 — резольвента дизъюнктов Dj0 и Dk0 , где j, k < i;3. либо Di0 — склейка дизъюнкта Dj0 , где j < i.Дизъюнкты D10 , D20 , . . . , Dn0 считаются резолютивновыводимыми из системы S.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.S = {D1 , D2 , D3 }D1 = P(x, f (y )) ∨ R(y ),D2 = ¬R(y ),D3 = ¬P(f (x), z) ∨ ¬P(y , y ).Резолютивный вывод из S1.2.3.4.5.6.D10D20D30D40D50D60= P(x1 , f (y1 )) ∨ R(y1 ), вариант дизъюнкта D1= ¬R(y2 ), вариант дизъюнкта D2= P(x3 , f (y3 )), резольвента дизъюнктов D10 , D20= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 ), вариант дизъюнкта D3= ¬P(f (x5 ), f (x5 )), склейка D40= , резольвента дизъюнктов D30 и D50Здесь — пустой дизъюнкт , тождественная ложь.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.А почему пустой дизъюнкт — это тождественная ложь?А потому, что каждый дизънкт D = L1 ∨ · · · ∨ Ln равносиленутверждению L1 ∨ · · · ∨ Ln ∨ false.Поэтому резольвентой дизъюнктов D1 = L ∨ false иD2 = ¬L ∨ false будет дизъюнкт D0 = false.Этот дизъюнкт не содержит ни одной литеры, и поэтомуназывается пустым дизънктом .РЕЗОЛЮТИВНЫЙ ВЫВОДОбратите внимание на то, что я постоянно переименовываюпеременные так, чтобы каждый дизъюнкт резолютивноговывода содержал свою индивидуальную систему переменных!Резолютивный вывод из S1.2.3.4.5.6.D10D20D30D40D50D60= P(x1 , f (y1 )) ∨ R(y1 )= ¬R(y2 )= P(x3 , f (y3 ))= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 )= ¬P(f (x5 ), f (x5 ))=Зачем это нужно?РЕЗОЛЮТИВНЫЙ ВЫВОДВсе дело в том, что все переменные дизъюнктов связаныкванторами ∀, и поэтому их имена можно достаточнопроизвольно изменять, полностью сохраняя смысл формул.Однако, случайное совпадение имен переменных (коллизия)может привести к тому, что резольвенту дизъюнктов построитьне удастся.Пусть S = {D1 = P(x), D2 = ¬P(f (x))}.1.

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

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