Skip to main content
SpringerLink
Log in
Book cover

European Conference on Computer Algebra

EUROCAL 1985: EUROCAL '85 pp 64–77Cite as

Fast subsumption algorithms

  • Automated Theorem Proving
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 204))

Abstract

Subsumption algorithms are used in resolution oriented theorem proving to eliminate redundant clauses from the search space. In a recent paper, the authors have introduced a new subsumption algorithm DC (Division into Components) which is much more efficient than the standard algorithms. In the present paper two new results are stated. First, an exponential lower bound for DC is presented. It is shown, that in certain cases DC is exponential in time, while IDC is only polynomial. However we prove when DC has polynomial time complexity, then also IDC is polynomial.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Blaesius K., Eisinger J., Smolka G., Herold A., Walther C.: The Markgraf Carl Refutation Procedure; Proc. IJCAI — 1981, Vancouver, 1981, pp 511–517.

    Google Scholar 

  2. Wos L.A.: Automated Reasoning: Real Uses and Potential Uses; Proc. IJCAI — 1983, Karlsruhe, 1983, vol.2, pp 867–876.

    Google Scholar 

  3. Garey M.R., Johnson D.S.: Computers and Intractability; Freeman & Comp., San Francisco, 1979.

    Google Scholar 

  4. Chang C.L., Lee R.C.T.: Symbolic Logic and Mechanical Theorem Proving; Academic Press, New York, 1973.

    Google Scholar 

  5. Stillman R.B.: The Concept of Weak Substitution in Theorem Proving; J.ACM 20 No 4, pp 23–41, 1973.

    Google Scholar 

  6. Gottlob G., Leitsch A.: On the Efficiency of Subsumption Algorithms; to appear in J.ACM, Vol.32,No.2, April 1985.

    Google Scholar 

  7. Loveland D.: Automated Theorem Proving: A Logical Basis; North Holland Publ. Comp., Amsterdam, 1978.

    Google Scholar 

  8. Paterson M.S., Wegman M.L.: Linear Unification; Journal of Comp. and Syst. Sciences, vol.16, No 2, pp 158–167, 1978.

    Google Scholar 

  9. Aho A.V., Hopcroft J.E., Ullman J.D.: Data Structures and Algorithms; Addison-Wesley Publ. Comp., 1983.

    Google Scholar 

  10. Robinson J.A.: A Machine-Oriented Logic Based on the Resolution Principle; J.ACM, vol.12, No 1, pp 23–41, 1965.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Istituto per la Matematica Applicata, C.N.R., Via L.B.Alberti, 4, 16132, Genova, Italy

    G. Gottlob

  2. Institut für Statistik, Wirtschaftsuniversität Wien, Augasse 2-6, 1090, Wien

    A. Leitsch

Authors
  1. G. Gottlob
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Leitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Bob F. Caviness

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gottlob, G., Leitsch, A. (1985). Fast subsumption algorithms. In: Caviness, B.F. (eds) EUROCAL '85. EUROCAL 1985. Lecture Notes in Computer Science, vol 204. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15984-3_239

Download citation

  • DOI: https://doi.org/10.1007/3-540-15984-3_239

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15984-1

  • Online ISBN: 978-3-540-39685-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation