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

66 k=1,…,m . Т.о. F противоречива тогда и только тогда, когда множество S противоречиво. Теорема доказана. Замечания. Пусть S - стандартная форма формулы F . Если F противоречива, то из доказанной теоремы следует, что F=S . Если F - непротиворечива, то вообще говоря F  S . Например: F: (  x)P(x), S:P(a) . S есть стандартная форма формулы F . Пусть I есть следующая интерпретация: D={1,2}, a=1, P(1)= Л,P(2)=И Тогда F истинна в I , но S ложна в I , т.е. F  S . Отметим, что формула может иметь более чем одну стандартную форму. Подстановка и унификация В методе резолюций существенным является нахождение контрарных пар. Для дизъюнктов, не содержащих функции это просто. Задача усложняется для дизъюнктов, содержащих функции. Пример 13.1. Найти контрарные пары. ( ) : ( ( )) : ( ) ( ) C P f x R x C P x Q x 2 1   Здесь нет контрарных пар. Но если в C 1 вместо x подставить f(a) , а в C 2 вместо x подставить a , то получим ( ) : ( ( )) ( ( )) : ( ( )) C P f a R a C P f a Q f a 2 1   Здесь ( ( )) P f a и ( ( )) P f a являются контрарными.