Предваренная форма. 
Системы поддержки принятия решений часть 1

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

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

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

• • исключить связки эквивалентности и импликации;
• • переименовать (если необходимо) связанные переменные таким образом, чтобы каждый квантор имел свою переменную;
• • удалить те квантификаторы, область действия которых не содержит квантифицированной переменной, как ненужные;
• • ограничить область действия отрицания;
• • п ровест и с колем изаци ю;
• • переместить все кванторы общности в начало формулы, образовав префикс и матрицу.

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