Наличие разноименных кванторов усложняет вывод заключения. Поэтому рассмотрим класс формул, содержащих только кванторы всеобщности. Формула F называется « — формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т.е.
F = «x1«x2 ¼«xn (M).
Для устранения кванторов существования из префикса формулы разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с другими предметными переменными.