Horn Clause

A Horn clause is disjunctions of literals s.t. at most one literal is positive. It could also be written in implicative form which is commonly used in Formal Methods.

• Exactly one positive literal: definite clause (strict Horn clause) $p\wedge q\wedge \dots \to t$
• No positive literal: goal clause $p\wedge q\wedge \dots \to \mathtt{false}$

And a fact is when there’s no negative literal:

$$\mathtt{true}\to t$$