1996
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

1995
Towards an Efficient Construction of Test Sets for Deciding Ground Reducability.
Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995