Horn Clauses

  • Alan Bundy
  • Lincoln Wallen
Part of the Symbolic Computation book series (SYMBOLIC)


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.




  1. [Chang and Keisier 73]
    Chang, C. C. and Keisier, H.J. Model Theory. North-Holland, 1973.Google Scholar
  2. [Kowalski 79]
    Kowaiski, R. A. Logic for problem solving. North-Holland, 1979.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Alan Bundy
    • 1
  • Lincoln Wallen
  1. 1.Department of Artificial IntelligenceEdinburgh UniversityEdinburghScotland

Personalised recommendations