9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций (В.А. Захаров - Лекции)

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