Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

S={Pv^Q v^, T, Q, Rv^v^Qv^U, Rv^T, -^v^Qv^T}. Выпишем дизъюнкты яз S ^ = S в ячейки нулевой строки нижеследующей таблицы. Каждая и - ая строка содержит дизъюнкты из S'^,n >0. Дизъюнкты, из которых строятся резольвенты, помечаем снизу звёздочками. На четвертом шаге получаем пустой дизъюнкт •, следовательно, множе­ ство S хорновских дизъюнктов невыполнимо. № итерации S" Дизъюнкты 0 S' Pv —iQ V—R T * Q Rv—Pv—iQv - i t / Rv^T * —Pv—iQv -1 Г* 1 S' Pv^Q T Q* Rv —Pv—iQv - i t / * R 2 Pv-P * T Q Rv—Pv —JJ R* 3 S' p* T Q Rv—Pv—iU R - i P * 4 S' • § 7. Преобразование формул логики предикатов. Сколемовская стаидарт- иая форма Из предыдуш,ей главы известно, что любую формулу логики предикатов А можно представить в предваренной (пренексной) нормальной форме, т. е. в ви- де: QiQi-'-QnB, где QhQ2,---,Qn - некоторая совокупность кванторов, а формула в не содержит кванторов. Для формулы А ~QiQ2---QnB совокупность кванторов QhQ2,---,Qn считает­ ся префиксом формулы А, а формула В - матрицей формулы А. В дальнейшем е этой главе считаем, что исходные формулы являются замкнутыми формулами. В логике предикатов указывалось, что матрицу формулы желательно при­ вести к к.н.ф. Напомним, что это означает. Элементарную формулу (атом) с от­ рицанием или без отрицания считают литерой или литералом в логике преди­ катов. Литерал считается позитивным литералом, если он не имеет отрицания и негативным, если содержит отрицание. Дизъюнкция литер или одна литера будет элементарной суммой в логике предикатов. Матрицу предваренной нормальной формы представляют в виде конъюнкции элементарных сумм, и эта конъюнкция называется конъюнктив­ ной нормальной формой (к.н.ф.) в логике предикатов. 69