References

For a complete list of references on Waldmeister see Th. Hillenbrands Homepage.

ALH00 J. Avenhaus, B. Löchner, and Th. Hillenbrand (2000)
On Using Ground Joinable Equations in Equational Theorem Proving
Baumgartner P., Zhang H., Proceedings of the 3rd International Workshop on First Order Theorem Proving (St Andrews, Scotland), Fachberichte Informatik 5/2000, pages 33-43. Universität Koblenz-Landau 2000.

BDP89 L. Bachmair, N. Dershowitz, D.A. Plaisted (1989)
Completion Without Failure
Ait-Kaci H., Nivat M., Resolution of Equations in Algebraic Structures, pages 1-30, Academic Press.

BG+92 L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder (1992)
Basic Paramodulation and Superposition
Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), pages 462-476, Lecture Notes in Artificial Intelligence 607, Springer-Verlag.

JLH99 A. Jaeger, B. Löchner, and Th. Hillenbrand (1999)
Waldmeister - Improvements in Performance and Ease of Use
Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), pages 232-236, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

LH02 B. Löchner, Th. Hillenbrand (2002)
The Next Waldmeister Loop
Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), pages 486-500, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

NR92 R. Nieuwenhuis, J.M. Rivero (1992)
Basic Superposition is Complete
Krieg-Brückner B., Proceedings of the 4th European Symposium on Programming (Rennes, France), pages 371-390, Lecture Notes in Computer Science 582, Springer-Verlag.

Further Reading...

KB70 D.E. Knuth and P.B. Bendix
Simple word problems in a universal algebra
In Resolutions of Equations in Algebraic Structures, volume 2, pages 1-30. Academic Press, 1989.

BDP89 L. Bachmair, N. Dershowitz, and D.A. Plaisted
Completion without failure
In Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970.

BH96 A. Buch and Th. Hillenbrand
Waldmeister: Development of a High Performance Completion-Based Theorem Prover
SEKI-Report SR-96-01.

HBF96 Th. Hillenbrand, A. Buch, and R. Fettig
On Gaining Efficiency in Completion-Based Theorem Proving
Proceedings RTA 96.

BHF96 A. Buch, Th. Hillenbrand, and R. Fettig
Waldmeister: High Performance Equational Theorem Proving
Proceedings DISCO 96.

HBVL97 Th. Hillenbrand, A. Buch, R. Vogt, and B. Löchner
Waldmeister: High-Performance Equational Deduction
Journal of Automated Reasoning, 18(2), 1997.

 

Copyright © 1998-2007 by Max-Planck-Institut für Informatik. All rights reserved.
Imprint and legal notices. www site design and concept by Doris Diedrich.
Document last changed on Friday, 27-Jun-2003 17:49:10 MEST.