TOPICS
Search

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

 L_1,...,L_n=>L(=¬L_1 v ... v ¬L_n v L)

or

 L_1,...,L_n=>(=¬L_1 v ... v ¬L_n),

where n>=0 and L 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.


See also

Clause

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

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.

Referenced on Wolfram|Alpha

Horn Clause

Cite this as:

Sakharov, Alex. "Horn Clause." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/HornClause.html

Subject classifications