Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

Research Interests

• High-performance theorem proving with the Waldmeister system.
• Higher-order rewriting and program transformations.

Major Publications

• Bernd Löchner: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting; Proc. 2nd IJCAR: 45-59 (2004).
• Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies: The New WALDMEISTER Loop at Work; Proc. 19th CADE : 317-321 (2003)
• Jürgen Avenhaus, Thomas Hillenbrand, Bernd Löchner: On using ground joinable equations in equational theorem proving; Journal of Symbolic Computation 36(1-2): 217-233 (2003)
• Thomas Hillenbrand, Bernd Löchner: The Next W ALDMEISTER Loop; Proc. 18th CADE: 486-500 (2002)
• Bernd Löchner, Thomas Hillenbrand: A phytography of WALDMEISTER; AI Commun. 15(2-3): 127-133 (2002)
• Jürgen Avenhaus, Bernd Löchner: CCE: Testing Ground Joinability; Proc. 1st IJCAR: 658-662 (2001)
• Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner: System Description: Waldmeister - Improvements in Performance and Ease of Use; Proc. 16th CADE 1999: 232-236 (1999)
• Jörg Denzinger, Bernd Löchner, Sebastian Scheffler: Unterstützung der Lehre durch Visualisierung von wissensbasierten Suchalgorithmen mit Java; Proc. Java-Informations-Tage: 180-191 (1998)
• Thomas Hillenbrand, Arnim Buch, Roland Vogt, Bernd Löchner: WALDMEISTER - High-Performance Equational Deduction; Journal of Automated Reasoning 18(2): 265-270 (1997)
• Roland Fettig, Bernd Löchner: Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus with Finite Products and terminal Type; Proc. 7th RTA: 347-361 (1996).

Unpublished

• Bernd Löchner: Joinability is Undecidable for Ordered Rewriting (2004) ps,ps.gz, pdf

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern