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)
- No positive literal: goal clause
And a fact is when there’s no negative literal: