A normal form for predicate calculus <189> formulae borrowed from mathematical logic, and much used in automatic theorem proving. It consists of applying prenex normal form, Skolemization <235> and conjunctive normal form, in succession. The resulting formula has a model if and only if the original formula does. A formula in clausal form consists of a conjunction of clauses. Each clause is a disjunction of literals. Each literal is either an atomic sentence or the negation of an atomic sentence, where an atomic sentence is a predicate applied to some terms.
- [Chang and Lee 73]Chang, C. and Lee, R. C. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973Google Scholar