Catalogue of Artificial Intelligence Techniques
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.
- Chang, C.C. and Keisler, H.J., Model Theory
, Elsevier North Holland, Amsterdam, 1973.