The QuodLibet Theorem Prover


After the death of Jürgen Avenhaus, our excellent teacher with a fascinating interest in the applicable logical side of theoretical computer science, this page is meant to provide some partial replacement for the original QuodLibet site that was part of Prof. Avenhaus' site on the server of Kaiserslautern University, which disappeared and seems to be lost.

Originally, this page was only on the following joint paper, but now we have added some further material at the bottom.

Our joint paper on the first system demonstration on an international conference

Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth
How to Prove Inductive Theorems? QuodLibet!
19th CADE 2003, LNAI 2741, pp. 328-333, Springer
Cite as
Bibtex Entry
Copyright Owner
QuodLibet is a tactic-based inductive theorem proving system that meets today's standard requirements for theorem provers such as a command interpreter, a sophisticated graphical user interface, and a carefully programmed inference machine kernel that guarantees soundness. In essence, it is the synergetic combination of the features presented in the following sections that makes QuodLibet a system quite useful in practice; and we hope that it is actually as you like it, which is the Latin ``quod libet'' translated into English. We start by presenting some of the design goals that have guided the development of QuodLibet. Note that the system is not intended to pursue the push bottom technology for inductive theorem proving, but to manage more complicated proofs by an effective interplay between interaction and automation.
Full paper
Orignal slides of the talk on QuodLibet at CADE, Miami, 2003
Slides of a QuodLibet Presentation in 2008

Further reading on QuodLibet (ordered by time of publication)

Screenshots and Photos