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.


Normal Form Conjunctive Normal Form Original Formula Automatic Theorem Prove Atomic Sentence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  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