# Catalogue of Artificial Intelligence Techniques

## Clausal Form

**Keywords:**
Horn clauses, Kowalski form, atomic
sentence, clause, conjunctive normal form, literals, logic programming, mathematical logic, prenex normal form, terms

### Categories: Knowledge Representation , Logic Programming , Theorem Proving

Author(s): **Alan Bundy, Martin Merry**

A normal form for Predicate Calculus formulae borrowed from mathematical logic, and much used in Automatic Theorem Proving. The clausal form of a formula is produced by first converting it into prenex normal form, Skolemising, and converting the result into conjunctive normal form. The final 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. Horn clauses are a very important subclass of clausal form formulas. They have at most one un-negated literal. Using the Kowalski form (where is written as ) they are formulas of the form:

where each of the and Q are atomic sentences. Horn clauses have several important properties when viewed from mathematical logic. In addition, they form the basis for the logic programming language Prolog: each predicate in a Prolog program has a Horn clause definition. The above formulae would be written:

respectively as Prolog programs.

### References:

- Chang, C.C. and Keisler, H.J.,
*Model Theory*, Elsevier North Holland, Amsterdam, 1973.

### Comments:

No comments.