Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

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.



Add Comment

No comments.