# 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 $\neg {P}_{1}^{}\vee \mathrm{...}\vee \neg {P}_{m}^{}\vee {Q}_{1}^{}\vee \mathrm{...}\vee {Q}_{n}^{}$ is written as ${P}_{1}^{}\&\mathrm{...}\&{P}_{m}^{}\to {Q}_{1}^{}\vee \mathrm{...}\vee {Q}_{n}^{}$ ) they are formulas of the form:

${P}_{1}^{}\&{P}_{2}^{}\&\dots \&{P}_{n}^{}\to Q\text{}or\text{}{P}_{1}^{}\&{P}_{2}^{}\&\dots \&{P}_{n}^{}\to$

where each of the ${P}_{i}^{}$ 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:

$Q\text{\hspace{0.17em}}:-\text{\hspace{0.17em}}P1,P2,\dots ,Pn.\text{}and\text{}$

respectively as Prolog programs.

### References:

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

### Comments:

No comments.