Advertisement

The Next Waldmeister Loop

  • Thomas Hillenbrand
  • Bernd Löchner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

In saturation-based theorem provers, the reasoning process consists in constructing the closure of an axiom set under inferences. As is well-known, this process tends to quickly fill the memory available unless preventive measures are employed. For implementations based on the Discount loop, the passive facts are responsible for most of the memory consumption. We present a refinement of that loop allowing such a compression that the space needed for the passive facts is linearly bound by the number of active facts. In practice, this will reduce memory consumption in the Waldmeister system by more than one order of magnitude as compared to previous compression schemes.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [ADF95]
    J. Avenhaus, J. Denzinger, and M. Fuchs. Discount: a system for distributed equational deduction. In J. Hsiang, ed., Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of LNCS, pp. 397–402. Springer-Verlag, 1995.Google Scholar
  2. [DP01]
    N. Dershowitz and D. A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume I, chapter 9, pp. 535–610. Elsevier, 2001.Google Scholar
  3. [Gra96]
    P. Graf. Term Indexing, volume 1053 of LNAI. Springer-Verlag, 1996.Google Scholar
  4. [Hil00]
    Th. Hillenbrand. Schnelles Gleichheitsbeweisen: Vom Vervollständigungskalkül zum Waldmeister-System. Diplomarbeit, Universität Kaiserslautern, Fachbereich Informatik, 2000. Available via http://www.mpi-sb.mpg.de/~hillen/documents/SchnellesBeweisen.ps.gz.
  5. [HL01]
    Th. Hillenbrand and B. Löchner. The next Waldmeister loop (extended abstract). In H. de Nivelle and S. Schulz, eds., Proceedings of the Second International Workshop on Implementation of Logics, Technical Report MPI-I-2001-2-006, pp. 13–21. Max-Planck-Institut für Informatik Saarbrücken, 2001.Google Scholar
  6. [Küc82]
    W. Küchlin. An implementation and investigation of the Knuth-Bendix completion procedure. Interner Bericht 17/82, Universität Karlsruhe, 1982.Google Scholar
  7. [LS01]
    B. Löchner and S. Schulz. An evaluation of shared rewriting. In H. de Nivelle and S. Schulz, eds., Proceedings of the Second International Workshop on Implementation of Logics, Technical Report MPI-I-2001-2-006, pp. 33–48. Max-Planck-Institut für Informatik Saarbrücken, 2001.Google Scholar
  8. [McC94]
    W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, 1994.Google Scholar
  9. [McC97]
    W. McCune. 33 basic test problems: a practical evaluation of some paramod-ulation strategies. In R. Veroff, ed., Automated Reasoning and its Applications: Essays in Honor of Larry Wos, chapter 5, pp. 71–114. MIT Press, 1997.Google Scholar
  10. [RSV01]
    I. V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume II, chapter 26, pp. 1853–1964. Elsevier, 2001.Google Scholar
  11. [RV00]
    A. Riazanov and A. Voronkov. Limited resource strategy in resolution theorem proving. Technical Report CSPP-7, University of Manchester, 2000. Accepted for publication in Journal of Symbolic Computation.Google Scholar
  12. [SS99]
    C.B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 99/02, James Cook University, Townsville, 1999.Google Scholar
  13. [Vor01]
    A. Voronkov. Algorithms, datastructures, and other issues in efficient automated deduction (invited talk). In R. Goré, A. Leitsch, and T. Nipkow, eds., Proceedings of the First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pp. 13–28. Springer-Verlag, 2001.Google Scholar
  14. [Wei01]
    Chr. Weidenbach. Combining superposition, sorts and splitting. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume II, chapter 27, pp. 1965–2013. Elsevier, 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Thomas Hillenbrand
    • 1
  • Bernd Löchner
    • 2
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany
  2. 2.FB InformatikUniversität KaiserslauternKaiserslauternGermany

Personalised recommendations