Clausal Form

  • Alan Bundy
  • Lincoln Wallen
Part of the Symbolic Computation book series (SYMBOLIC)


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.




  1. [Chang and Lee 73]
    Chang, C. and Lee, R. C. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Alan Bundy
    • 1
  • Lincoln Wallen
  1. 1.Department of Artificial IntelligenceEdinburgh UniversityEdinburghScotland

Personalised recommendations