## Abstract

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.

## Keywords

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.

## Reference

- [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