Horn Clauses

Abstract

Horn Clauses are formulae of first order predicate calculus <189> of the form:

$$ {\rm{A1}}\,\,{\rm{\& }}\,\,{\rm{A2}}\,\,{\rm{\& }}\,\,{\rm{.}}\,\,{\rm{.}}\,\,{\rm{.}}\,\,{\rm{\& }}\,{\rm{An}}\,\,{\rm{A}}\,\,\,\,\,{\rm{or}}\,\,\,\,{\rm{A1}}\,\,{\rm{\& }}\,\,{\rm{A2}}\,\,{\rm{\& }}\,\,{\rm{.}}\,\,{\rm{.}}\,\,{\rm{.}}\,\,{\rm{\& }}\,\,{\rm{An}}\,\, \to $$

where each of the Ai and A are atomic formulae i.e. of the form R(C1.....Cn), where R is a relation, each Cj is a term, and n ≥. 0.