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

50 1 2 : ( ( )) : _______________ : ? F p q rs F pqr G s    Используя теорему 9.2, получаем         pqr s F F G p q rs 1 2 ( ( )) ( ) (          ) ( )) ( ) ( ( )) ( ( pqrs pqrs p q rs p q rs pqrs pqrs 0    ) ) ( ( и, следовательно, заключение G является верным. 10. Метод резолюций для исчисления высказываний Метод резолюций для исчисления высказываний Определение. Дизъюнктом называется дизъюнкция пропозициональных переменных. Определение. Пропозициональные переменные p и p называются контрарными. Определение. Для любых двух дизъюнктов C 1 и C 2 , если существует переменная  1 в C 1 , которая контрарна переменной  2 в C 2 , то вычеркнув  1 и  2 из C 1 и C 2 соответственно, и построив дизъюнкцию оставшихся дизъюнктов, получим резольвенту C 1 и C 2 . Определение. Дизъюнкт, не содержащий переменных, называется пустым (обозначаем П ). Такой дизъюнкт по определению противоречив.