Skip to main content
SpringerLink
Log in

On the Evaluation of Indexing Techniques for Theorem Proving

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2083))

Included in the following conference series:

Abstract

The problem of term indexing can be formulated abstractly as follows (see [19]). Given a set L of indexed terms, a binary relation R over terms (called the retrieval condition) and a term t (called the query term), identify the subset M of L that consists of the terms l such that R(l; t) holds. Terms in M will be called the candidate terms. Typical retrieval conditions used in first-order theorem proving are matching, generalization, unifiability, and syntactic equality. Such a retrieval of candidate terms in theorem proving is interleaved with insertion of terms to L, and deletion of them from L.

Partially supported by the Spanish CICYT project HEMOSS ref. TIC98-0949-C02- 01.

Acknowledgments

We thank Jürgen Avenhaus for valuable remarks to yesterday’s version of this paper which was as a result substantially rewritten today.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Cheeseman, B. Kanefsky, and W. M. Taylor. Where the really hard problems are. In R. Reiter J. Mylopoulos, editor, IJCAI 1991. Proceedings of the 12th International Joint Conference on Artificial Intelligence, pages 331–340, Sydney, Australia, 1991. Morgan Kaufmann.

    Google Scholar 

  2. J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95–113, February 1993.

    Article  MathSciNet  Google Scholar 

  3. H. Ganzinger, R. Nieuwenhuis, and P. Nivela. Context trees. In IJCAR 2001, Proceedings of the International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, Siena, Italy, June 2001. Springer Verlag.

    Google Scholar 

  4. P. Graf. Extended path-indexing. In A. Bundy, editor, CADE-12. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 514–528, Nancy, France, June/July 1994.

    Google Scholar 

  5. P. Graf. Substitution tree indexing. In J. Hsiang, editor, Procs. 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 117–131, Kaiserslautern, 1995.

    Chapter  Google Scholar 

  6. P. Graf. Term Indexing, volume 1053 of Lecture Notes in Computer Science. Springer Verlag, 1996.

    Google Scholar 

  7. J. Gu, P.W. Purdom, J. Franco, and B.W. Wah. Algorithms for the Satisfiability Problems. Cambridge University Press, 2001.

    Google Scholar 

  8. C. Hewitt. Description and theoretical analysis of Planner: a language for proving theorems and manipulating models in a robot. PhD thesis, Department of Mathematics, MIT, Cambridge, Mass., January 1971.

    Google Scholar 

  9. T. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. Waldmeister: High-performance equational deduction. Journal of Automated Reasoning, 18(2):265–270, 1997.

    Article  Google Scholar 

  10. A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

    Article  MATH  Google Scholar 

  11. W.W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147–167, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  12. W.W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, January 1994.

    Google Scholar 

  13. D.G. Mitchell, B. Selman, and H.J. Levesque. Hard and easy distributions of SAT problems. In W.R. Swartout, editor, Procs. 10th National Conference on Artificial Intelligence, pages 459–465, San Jose, CA, January 1992. AAAI Press/MIT Press.

    Google Scholar 

  14. R. Nieuwenhuis. Rewrite-based deduction and symbolic constraints. In H. Ganzinger, editor, CADE-16. 16th Int. Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 302–313, Trento, Italy, July 1999.

    Google Scholar 

  15. R. Nieuwenhuis, J.M. Rivero, and M.Á. Vallejo. The Barcelona prover. Journal of Automated Reasoning, 18(2):171–176, 1997.

    Article  Google Scholar 

  16. H.J. Ohlbach. Abstraction tree indexing for terms. In H.-J. Börkert and W. Nutt, editors, Extended Abstracts of the Third International Workshop on Unification, pages 131–135. Universität Kaiserslautern, 1989. SEKI-Report SR 89-17.

    Google Scholar 

  17. M. Paterson and M. Wegman. Linear unification. Journal of Computer and System Sciences, 16:158–167, 1978.

    Article  MathSciNet  MATH  Google Scholar 

  18. P.W. Purdom and C.A. Brown. Fast many-to-one matching algorithms. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, First International Conference, RTA-85, volume 202 of Lecture Notes in Computer Science, pages 407–416, Dijon, France, 1985. Springer Verlag.

    Chapter  Google Scholar 

  19. I.V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 1–97. Elsevier Science and MIT Press, 2001. To appear.

    Google Scholar 

  20. A. Riazanov and A. Voronkov.Vampire. In H. Ganzinger, editor, CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 292–296, Trento, Italy, July 1999.

    Google Scholar 

  21. A. Riazanov and A. Voronkov. Partially adaptive code trees. In M. Ojeda-Aciego, I.P. de Guzmán, G. Brewka, and L.M. Pereira, editors, Logics in Artificial Intelligence. European Workshop, JELIA 2000, volume 1919 of Lecture Notes in Artificial Intelligence, pages 209–223, Málaga, Spain, 2000. Springer Verlag.

    Google Scholar 

  22. J.M.A. Rivero. Data Structures and Algorithms for Automated Deduction with Equality. Phd thesis, Universitat Politèecnica de Catalunya, Barcelona, May 2000.

    Google Scholar 

  23. S. Schulz. Learning Search Control Knowledge for Equational Deduction, volume 230 of Dissertationen zur könstliche Intelligenz. Akademische Verlagsgesellschaft Aka GmmH, 2000.

    Google Scholar 

  24. M. Stickel. The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989.

    Google Scholar 

  25. G. Sutcliffe and C. Suttner. The TPTP problem library — CNF release v. 1.2.1. Journal of Automated Reasoning, 21(2), 1998.

    Google Scholar 

  26. A. Voronkov. The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Automated Reasoning, 15(2):237–265, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  27. A. Voronkov. CASC 16 1/2. Preprint CSPP-4, Department of Computer Science, University of Manchester, February 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Catalonia, Spain

    Robert Nieuwenhuis

  2. Universität Kaiserslautern, Germany

    Thomas Hillenbrand

  3. University of Manchester, UK

    Alexandre Riazanov & Andrei Voronkov

Authors
  1. Robert Nieuwenhuis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Hillenbrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandre Riazanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev Goré

  2. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria

    Alexander Leitsch

  3. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A. (2001). On the Evaluation of Indexing Techniques for Theorem Proving. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-45744-5_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42254-9

  • Online ISBN: 978-3-540-45744-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation