Skip to main content
SpringerLink
Log in

Adaptive Saturation-Based Reasoning

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2001)

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

Abstract

For most applications of first-order theorem provers a proof should be found within a fixed time limit. When the time limit is set, systems can perform much better by using algorithms other than the ordinary complete ones. In this paper we describe the Limited Resource Strategy intended to improve performance of resolution- and paramodulation- based provers when a fixed limit is imposed on the time of a run. We give experimental evidence that the Limited Resource Strategy gives a significant improvement over the OTTER saturation algorithm, algorithms not using passive clauses for simplification and the weightbased algorithms.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT: a system for distributed equational deduction. In J. Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA—95), volume 914 of Lecture Notes in Computer Science, pages 397–402, Kaiserslautern, 1995.

    Google Scholar 

  2. H. de Nivelle. Bliksem 1.10 User’s Manual. MPI für Informatik, Saarbrücken, 2000.

    Google Scholar 

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

    Google Scholar 

  4. Th. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. Waldmeister: Highperformance equational deduction. Journal of Automated Reasoning, 18(2):265–270, 1997.

    Article  Google Scholar 

  5. E.L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In A. Voronkov, editor, Logic Programming and Automated Reasoning. International Conference LPAR’92., volume 624 of Lecture Notes in Artificial Intelligence, pages 96–106, St.Petersburg, Russia, July 1992.

    Google Scholar 

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

    Google Scholar 

  7. M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO-the CADE-13 systems. Journal of Automated Reasoning, 18:237–246, 1997.

    Article  Google Scholar 

  8. I.V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 26, pages 1853–1964. Elsevier Science, 2001.

    Google Scholar 

  9. A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Automated Deduction-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 

  10. A. Riazanov and A. Voronkov. Vampire 1.1 (system description). In R. Gore, A. Leitsch, and T. Nipkow, editors, Automated Reasoning. First International Joint Conference, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 376–380, Siena, Italy, June 2001.

    Google Scholar 

  11. S. Schulz. System abstract: E 0.61. In R. Gore, A. Leitsch, and T. Nipkow, editors, Automated Reasoning. First International Joint Conference, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 370–375, Siena, Italy, June 2001.

    Google Scholar 

  12. J. Schumann and B. Fischer. NORA/HAMMR: Making deduction-based software component retrieval practical. In Proc. Automated Software Engineering (ASE-97), pages 246–254, Lake Tahoe, November 1997. IEEE Computer Society Press.

    Google Scholar 

  13. G. Sutcliffe. The CADE-16 ATP system competition. Journal of Automated Reasoning, 2000. to appear.

    Google Scholar 

  14. T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199–204, 1997.

    Article  Google Scholar 

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

    Google Scholar 

  16. C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. System description: Spass version 1.0.0. In H. Ganzinger, editor, Automated Deduction—CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 378–382,Trento, Italy, July 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, USA

    Alexandre Riazanov & Andrei Voronkov

Authors
  1. Alexandre Riazanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Informatics and Mathematical Modelling, Technical University of Denmark, Bldg.322, 106-108, Richard Petersens Plads, 2800, Lyngby, Denmark

    Dines Bjørner

  2. Computer Science Department, Technical University of Munich, Arcisstr.21, 80290, Munich, Germany

    Manfred Broy

  3. A.P.Ershov Institute of Informatics Systems, Acad.Lavrentjev ave.,6, 630090, Novosibirsk, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Riazanov, A., Voronkov, A. (2001). Adaptive Saturation-Based Reasoning. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2001. Lecture Notes in Computer Science, vol 2244. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45575-2_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-45575-2_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation