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: