Предваренная форма

Полученная только что, после сколемизации, формула имеет вполне определенный вид. Она состоит из цепочки кванторов, называемой префиксом и бескванторной формулы, называемой матрицей. Представить какую-либо формулу в виде префикса и матрицы - это значит представить ее в предваренной форме. Особенность предваренной формы в том, что все кванторы оказываются вынесенными влево за пределы общей формулы, а часть, оставшаяся без кванторов, может быть подвергнута всем возможным преобразованиям, в частности, быть представленной в конъюнктивной нормальной форме, такой необходимой нам для реализации принципа резолюции.

Для любой логической формулы существует логически эквивалентная ей предваренная форма.

Это правило вытекает из тех преобразований, которые необходимо для этого проделать - они известны и всегда выполнимы:

¨ исключить связки эквивалентности и импликации;

¨ переименовать (если необходимо) связанные переменные
таким образом, чтобы каждый квантор имел свою переменную;

¨ удалить те квантификаторы, область действия которых не содержит квантифицированной переменной, как ненужные;

¨ ограничить область действия отрицания;

¨ провести сколемизацию;

¨ переместить все кванторы общности в начало формулы, образовав префикс и матрицу.

К моменту последней операции перемещения кванторов связанные переменные уже разделены, каждый квантор общности имеет свою переменную, независимые переменные заменены постоянными (конкретизация). Будучи перемещенным в начало формулы, он и все равно распространяют влияние лишь на "свои" переменные. Широко используются приведенные ранее равносильности (6.1) - (6.7). Может пригодиться еще и правило раскрытия импликации:

x (A (x) B (x)) =xA (x) xB (x). (6.8)

Дата добавления: 2014-01-20