Deciding Horn classes by hyperresolution

  • Alexander Leitsch
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


It is shown that positive hyperresolution can be used as decision procedure for solvable classes of Horn clause sets. Rather than by quantifier prefixes or by propositional features these classes are characterized by variable occurrence — and term depth properties. Special attention is given to a subclass of the Horn clause implication problem, which can be represented as consistency problem; to decide ∀C→∀D, ( ∀C denotes the universal closoure of C, C is a Horn clause, D is an arbitrary clause ) we apply hyperresolution to the clause form of ∀C∧⌍∀D. Special techniques can be used in handling such implication clause forms, because there is only one rule, ground unit facts and ground unit goals. The sharp boundary between solvable and unsolvable classes is illustrated, and a complexity analysis of some classes is given.


Decision Procedure Function Symbol Horn Clause Ground Term Unit Clause 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [CL 73]
    C. L. Chang & R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press 1973.Google Scholar
  2. [DG 79]
    B. Dreben & W. D. Goldfarb: The Decision Problem — Solvable Classes of Quantificational Formulas, Addison Wesley 1979.Google Scholar
  3. [Fe 89]
    C.Fermüller: Deciding some Horn Clause Sets by Resolution, to appear in the Yearbook of the Kurt Gödel Society 1989.Google Scholar
  4. [GJ 79]
    M. R. Garey & D. S. Johnson: Computers and Intractability; Freeman & Comp., San Francisco, 1979.Google Scholar
  5. [Go 87]
    G. Gottlob: Subsumption and Implication, Information Processing Letters 24 (1987), 109–111.Google Scholar
  6. [Jo 76]
    W. H. Joyner jr.: Resolution Strategies as Decision Procedures, JACM Vol 23 No. 3, (July 1976), 398–417.CrossRefGoogle Scholar
  7. [Lei 88]
    A. Leitsch: Implication Algorithms for Classes of Horn Clauses, Statistik, Informatik + Oekonomie, Springer Verl. Berlin, Heidelberg, 1988, 172–189.Google Scholar
  8. [LG 89]
    A.Leitsch, G.Gottlob: Deciding Horn Clause Implication by Ordered Semantic Resolution, to appear in Proc. Intern. Symp. Computational Intelligence 89, Elsevier 1989.Google Scholar
  9. [Lew 79]
    H.R. Lewis: Unsolvable Classes of Quantificational Formulas, Addison Wesley 1979.Google Scholar
  10. [Lo 78]
    D. Loveland: Automated Theorem Proving — A Logical Basis, North Holland Publ. Comp. 1978.Google Scholar
  11. [MM 82]
    A. Martelli, U. Montanari: An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, Vol. 4 No. 2, (April 1982).Google Scholar
  12. [Si 84]
    J. Siekmann: Universal Unification, 7th International Conference on Automated Deduction, LNCS 170(1984),1–42.Google Scholar
  13. [SS 88]
    M. Schmidt-Schauss: Implication of Clauses is Undecidable, Theoretical Computer Science 59 (1988), 287–296.Google Scholar
  14. [ST 71]
    S. Stenlund: Combinators, λ-Terms and Proof Theory, Reidel Publ. Comp. 1971.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Alexander Leitsch
    • 1
  1. 1.Institut für Praktische InformatikTechnical University of ViennaViennaAustria

Personalised recommendations