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. Bibtex Entry
Copyright Owner
Yes! April 9, 2003
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.
Tobias Schmidt-Samoa and Claus-Peter Wirth
Full paper
Slides of Talk CADE, Miami, 2003
Slides of a Presentation in 2008