Abstract
We present recent developments within the equational theorem prover Waldmeister, an implementation of unfailing Knuth-Bendix completion [BDP89] with refinements towards ordered completion. The new developments rely on a novel organization of the underlying saturation-based proof procedure into a system architecture. As is known, the saturation process tends to quickly fill the memory available unless preventive measures are employed. To overcome this problem, our new “Waldmeister loop” features a highly compact representation of the search state, exploiting its inherent structure. The implementation just being available, the cost and the benefits of the concept now can exactly be measured. Indeed are our expectations met concerning the drastic cut-down of memory usage with only moderate overhead of time.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press, London (1989)
Bündgen, R., Göbel, M., Küchlin, W., Weber, A.: Parallel term rewriting with PaReDuX. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction—A Basis for Applications: Systems and Implementation Techniques, vol. II, pp. 231–260. Kluwer Academic Publishers, Dordrecht (1998)
Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence 29(1–4), 223–257 (2000)
Denzinger, J., Fuchs, D.: Cooperation of heterogeneous provers. In: Dean, T. (ed.) Proceedings of the 16th International Joint Conference on Artificial Intelligence, pp. 10–15. Morgan Kaufmann, San Francisco (1999)
Hillenbrand, T., Löchner, B.: The next Waldmeister loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 486–500. Springer, Heidelberg (2002)
Löchner, B., Hillenbrand, T.: A phytography of Waldmeister. AI Communications 15(2,3), 127–133 (2002)
McCune, W.: 33 basic test problems: a practical evaluation of some paramodulation strategies. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, pp. 71–114. MIT Press, Cambridge (1997)
Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Tech. Report CSPP-7, University of Manchester (2000)
Suttner, C.B., Sutcliffe, G.: The TPTP problem library (TPTP v2.2.0). Tech. Report 99/02, James Cook University, Townsville (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gaillourdet, JM., Hillenbrand, T., Löchner, B., Spies, H. (2003). The New WALDMEISTER Loop at Work. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive