Как и в случае пропозициональной логики, для резолюции в логике первого порядка требуется, чтобы высказывания находились в конъюнктивной нормальной форме (Conjunctive Normal Form— CNF), т.е. представляли собой конъюнкцию выражений, в которой каждое выражение представляет собой дизъюнкцию литералов6. Литералы могут содержать переменные, на которые, согласно принятому предположению, распространяется квантор всеобщности. Например, высказывание

принимает в форме CNF следующий вид:

Каждое высказывание в логике первого порядка может быть преобразовано в эквивалентное с тонки зрения логического вывода высказывание CNF. В частности, высказывание CNF является невыполнимым тогда и только тогда, когда невыполнимо первоначальное высказывание, поэтому мы получаем основу для формирования доказательств от противного с помощью высказываний CNF.

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

Ниже приведены этапы этого преобразования.