Horn clause

A Horn clause is a logical disjunction of literals, where at most one of the literals is positive, and all others are negative. It is named after Alfred Horn, who first described them in a 1951 article.

A Horn clause with exactly one positive literal is known as a definite clause. If a definite clause has no negative literals, it is sometimes referred to as a "fact." Conversely, a Horn clause without any positive literals is often called a goal clause.These three kinds of Horn clauses are shown in the following propositional example:

definite clause: ${\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}$

is an example of a definite Horn clause. Here's how to interpret it: