- Tobias Schmidt-Samoa
- The New Standard Tactics of the Inductive Theorem Prover
- SEKI-Report SR-2004-01
- Copyright Owner
is a tactic-based inductive theorem prover for the verification
of algebraic specifications of algorithms in the style of abstract
data types with positive/negative-conditional equations.
Its core system consists of a small inference machine kernel that
merely acts as a proof checker.
Automation is achieved with tactics written in QML
(QuodLibet-Meta-Language), an adapted imperative programming language.
In this paper, we describe QuodLibet's new standard tactics, a pool of
general purpose tactics provided with the core system that support
the user in proving inductive theorems.
We aim at clarifying the underlying ideas as well as explaining the
parameters with which the user can influence the behavior of the
tactics during the proof process.
One of the major achievements of this paper is the application of
conditional lemmas controlled by obligatory and mandatory literals.
This has drastically improved the degree of automation without
increasing the runtime significantly as will be illustrated by the
Nevertheless, the degree of automation depends on the specification
Thus, we will also give some guidelines how to write specifications
and how to use the new tactics efficiently.
- Reviewed by Claus-Peter Wirth
- Full paper
- .3 Mbytes
- The titlepage does not work in the following dvi version!
- .1 Mbytes
- The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
- .5 Mbytes