Horn Clause

A clause (i.e., a disjunction of literals) is called a Horn clause if it contains at most one positive literal. Horn clauses are usually written as

or

where  and  is the only positive literal.

A definite clause is a Horn clause that has exactly one positive literal. A Horn clause without a positive literal is called a goal.

Horn clauses express a subset of statements of first-order logic. Programming language Prolog is built on top of Horn clauses. Prolog programs are comprised of definite clauses and any question in Prolog is a goal.

REFERENCES

Clocksin, W. F. and Mellish, C. S. Programming in Prolog Using the ISO Standard. New York: Springer-Verlag, 1984.

Horn, A. "On Sentences Which Are True of Direct Unions of Algebras." J. Symbolic Logic 16, 14-21, 1951.