On Gaining Efficiency in Completion-Based Theorem Proving.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996
Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996
WALDMEISTER: High Performance Equational Theorem Proving.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996
Towards an Efficient Construction of Test Sets for Deciding Ground Reducability.
Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995