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.


Horn Clause Fourier Descriptor Prolog Program Clause Definition Quad Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  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