k variables by two conjuncts and with a new variable, and repeating as often as necessary. Converting from first-order logic To convert first-order logic to CNF: Convert to negation normal form. Eliminate implications and equivalences: repeatedly replace with ; replace with . Eventually, this will eliminate all occurrences of and . Move NOTs inwards by repeatedly applying De Morgan's law. Specifically, replace with ; replace with ; and replace with ; replace with ; with . After that, a may occur only immediately before a predicate symbol. Standardize variables For sentences like which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example, is renamed to . Skolemize the statement Move quantifiers outwards: repeatedly replace with ; replace with ; replace with ; replace with . These replacements preserve equivalence, since the previous variable standardization step ensured that doesn't occur in . After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a , , or . Repeatedly replace with , where is a new -ary function symbol, a so-called "Skolem function". This is the only step that preserves only satisfiability rather than equivalence. It eliminates all existential quantifiers. Drop all universal quantifiers. Distribute ORs inwards over ANDs: repeatedly replace with . As an example, the formula saying "Anyone who loves all animals, is in turn loved by someone" is converted into CNF (and subsequently into clause form in the last line) as follows (highlighting replacement rule redexes in ): Informally, the Skolem function can be thought of as yielding the person by whom is loved, while yields the animal (if any) that doesn't love. The 3rd last line from below then reads as " doesn't love the animal , or else is loved by ". The 2nd last line from above, , is the CNF. Notes See also Algebraic normal form Disjunctive normal form Horn clause Quine–McCluskey algorithm References Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits. In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198 G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic,