@InProceedings{quodlibet,
author ={J{\"u}rgen Avenhaus
and Ulrich K{\"u}hler
and Tobias Schmidt-Samoa
and Claus-Peter Wirth},
title ={How to Prove Inductive Theorems? {QuodLibet}!},
pages ={328--333},
year ={2003},
booktitle ={Proceedings of the 19th International Conference on
{A}utomated {D}eduction (CADE-19)},
publisher ={Springer},
series ={Lecture Notes in Artificial Intelligence},
number ={2741},
editor ={Franz Baader},
note ={{\url{www.ags.uni-sb.de/~cp/p/quodlibet/welcome.html}}},
abstract ={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.}}