Математическая логика и теория алгоритмов

Дизъюнкты, из которых строятся резольвенты, помечаем снизу звез­ дочками. Но­ мер ите- ра-" щга S" Дизъюнкты 0 S ° P v l f i v l y ? T • Q RS A PS A QS A U RV]T * i P v i e v i T - * 1 s ' * T Q * RSA P V 1 QVI И * R l ? v l O * 2 * T Q RvlPv^ И R * ^P 3 s ' p • T Q y?vlPv1 И R ^P * 4 • На четвертом шаге получаем пустой дизъюнкт •, следовательно, множество S хорновских дизъюнктов невыполнимо. § 8, Преобразование формул логики предикатов. Сколемовская стандартная форма Из предыдущей главы известно, что любую формулу логи­ ки предикатов можно представить в предваренной нормальной форме, т.е. в виде; QiQb.-Qtfi, где QhQ2,...,Qn - некоторая совокупность кван­ торов, а формула В не содержит кванторов, 102