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

52 Теорема 10.1. Пусть даны два дизъюнкта C 1 и С 2 . Тогда резольвента С дизъюнктов C 1 и С 2 есть их логическое следствие. Доказательство. Пусть дизъюнкты C 1 и С 2 содержат контрарную пару переменных  и  , т.е. 1 1 C C     и 2 2 C C     , где 1 C  и 2 C  – некоторые дизъюнкты. Пусть также 2 1 C C C     – резольвента C 1 и С 2 . Пусть C 1 и С 2 истинны в некоторой интерпретации I . Нужно показать, что резольвента C дизъюнктов C 1 и С 2 также истинна в I . Прежде всего либо  , либо  ложны в I . Пусть  ложна в I . Тогда дизъюнкт C 1 должен содержать более одной переменной, иначе C 1 был бы ложен в I . Следовательно 1 C  должен быть истинен в I . Таким образом, резольвента 2 1 C C C     истинна в I . Аналогично можно показать, что если  ложна в I , то 2 C  должен быть истинен в I , а, следовательно, и 2 1 C C C     должна быть истинна в I . Теорема доказана. Определение. Пусть S – множество дизъюнктов. Резолютивный вывод C из S есть такая конечная последовательность C 1 ,C 2 ,…,C k дизъюнктов, что C k =C , а каждый C i или принадлежит S или является резольвентой дизъюнктов, предшествующих C i . Если существует вывод C из S , то C (по теореме 10.1) является логическим следствием S . Кроме того, если C= П, то s 1 &s 2 &…&s n – противоречие. Здесь { s 1 ,s 2 ,…,s n } =S . Пример 10.5. Является ли резольвента логическим следствием? , , } { S p q q p   . Резолютивный вывод: