- Authors
-
Jürgen Avenhaus,
Ulrich Kühler,
Tobias Schmidt-Samoa,
Claus-Peter Wirth
- Title
- How to Prove Inductive Theorems?
QuodLibet!
- In
- 19th CADE 2003, LNAI 2741, pp. 328-333, Springer.
Bibtex Entry
- Copyright Owner
- Springer
- Up-to-dateness
- Yes! April 9, 2003
- 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.
- Photos
- Tobias Schmidt-Samoa and Claus-Peter Wirth
- Full paper
-
- Format
- .ps.gz
- Size
- .02 Mbytes
-
- Format
- .dvi.gz
- Size
- .06 Mbytes
-
The fonts of this version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
- Format
- .pdf
- Size
- .05 Mbytes
- Slides of Talk CADE, Miami, 2003
-
-
- Format
- PDF
- Size
- .4 Mbytes
- For poor beamers: No background colors.
- Format
- PDF level 1.3
- Size
- .3 Mbytes
- For printing: No background colors and accumlated overlays:
- Format
- PS.GZ
- Size
- .5 Mbytes
- Slides of a Presentation in 2008
-
-
- Format
- PDF
- Size
- .4 Mbytes
- For poor beamers: No background colors.
- Format
- PDF
- Size
- .2 Mbytes
- For printing: No background colors and accumlated overlays:
- Format
- PS.GZ
- Size
- .4 Mbytes