Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type. - Roland Fettig; Bernd Löchner (RTA, 1996)

WALDMEISTER - High-Performance Equational Deduction. - Thomas Hillenbrand; Arnim Buch; Roland Vogt; Bernd Löchner (J. Autom. Reason., 1997)

Unterstützung der Lehre durch Visualisierung von wissensbasierten Suchalgorithmen mit Java. - Jörg Denzinger; Bernd Löchner; Sebastian Scheffler (Java-Informations-Tage, 1998)

System Description: Waldmeister - Improvements in Performance and Ease of Use. - Thomas Hillenbrand; Andreas Jaeger; Bernd Löchner (CADE, 1999)

CCE: Testing Ground Joinability. - Jürgen Avenhaus; Bernd Löchner (IJCAR, 2001)

The Next W ALDMEISTER Loop. - Thomas Hillenbrand; Bernd Löchner (CADE, 2002)

A phytography of WALDMEISTER. - Bernd Löchner; Thomas Hillenbrand (AI Commun., 2002)

The New WALDMEISTER Loop at Work. - Jean-Marie Gaillourdet; Thomas Hillenbrand; Bernd Löchner; Hendrik Spies (CADE, 2003)

On using ground joinable equations in equational theorem proving. - Jürgen Avenhaus; Thomas Hillenbrand; Bernd Löchner (J. Symb. Comput., 2003)

A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. - Bernd Löchner (IJCAR, 2004)

Advances in equational theorem proving: architecture, algorithms, and redundancy avoidance. - Bernd Löchner (2005)

Things to Know When Implementing Lpo. - Bernd Löchner (Int. J. Artif. Intell. Tools, 2006)

Knuth-Bendix completion of theories of commuting group endomorphisms. - Aaron Stump; Bernd Löchner (Inf. Process. Lett., 2006)

Things to Know when Implementing KBO. - Bernd Löchner (J. Autom. Reason., 2006)