Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

69 14. Метод резолюций в исчислении предикатов Метод резолюций в исчислении предикатов Определение. Атомарная формула есть литера. Определение. Если две или более литер (с одинаковым знаком) дизъюнкта C имеют общий унификатор  , то C  называется склейкой C . Если C  – единичный дизъюнкт, то склейка называется единичной склейкой. Пример 14.1. Пусть ( ) ( ) ( ( )) C P x P f y Q x    . Тогда подчеркнутые литеры имеют общий унификатор { ( ) / } f y x   . Следовательно, ( ( )) ( ( )) ( ( )) ( ( )) ( ( )) C P f y P f y Q f y P f y Q f y       есть склейка C . Определение. Пусть C 1 и C 2 – два дизъюнкта, которые не имеют никаких общих переменных. Пусть L 1 и L 2 – две литеры в C 1 и C 2 соответственно. Если L 1 и 2 L имеют общий унификатор  , то дизъюнкт (C 1  | L 1  )  (C 2  | L 2  ) называется бинарной резольвентой C 1 и C 2 . Литеры L 1 и L 2 называются отрезаемыми литерами. Пример 14.2. Пусть ( ) ( ) C P x Q x 1   , а ( ) ( ) C P a R x 2   . Т.к. x входит в C 1 и C 2 , то заменяем переменную x в C 2 и пусть ( ) ( ) C P a R y 2   . Выбираем L 1 =P(x), ( ) L P a 2  .Т.к. ( ) L P a 2  , то L 1 и 2 L имеют унификатор  = {a | x} . Следовательно