- Ulrich Kühler
- A Tactic-Based Inductive Theorem Prover for Data Types with
- PhD thesis, ISBN 3-89838-238-9, Infix,
Akademische Verlagsgesellschaft Aka GmbH,
- Copyright Owner
- Akademische Verlagsgesellschaft Aka GmbH, Berlin
- Data types such as the natural numbers, lists, strings, trees, graphs etc.
are essential for the design and implementation of most software systems.
A given data type $D$ can often be adequately formalized
using an equational specification $spec$ with inductive semantics
(i.e. the carriers of the models associated with $spec$ as the semantics of $spec$
are inductively defined).
This entails that
statements expressing valid properties of the operations of $D$
are represented by the inductive theorems of the specification $spec$.
inductive theorem proving constitutes the basis of
a suitable formal method for reasoning about data types.
The subject of this thesis is an inductive theorem prover
which we have developed to attain two essential goals.
our prover is applicable to data types with partial operations,
although data types like these lead to specifications
that need not be sufficiently complete or may induce non-terminating rewrite relations.
by offering a high degree of flexibility with regard to
the supported forms of proof control,
the tactic-based approach to the problem of proof control developed for
yields a practically useful compromise
between interactive proof control on the one hand
and automated proof control on the other hand.
In the first part of this thesis,
we present a comprehensive and rewrite-based
formal framework for inductive theorem proving
which serves as the logical foundations of QuodLibet.
The main components of this framework are
(i) an algebraic specification language for the formalization of data types,
(ii) a ``semantic'' induction order for guaranteeing
applicability of induction hypotheses,
(iii) a calculus for inductive proofs for formal reasoning about data types and
(iv) a concept of a so-called proof state graph for the adequate representation
of proof constructions.
the specification language allows axioms to be conditional equations (or rewrite rules)
with positive and negative conditions,
and it has precisely defined admissibility conditions,
which can be easily verified for most practically relevant specifications
(as no proofs of termination are required).
by incorporating proof state graphs,
our framework is capable of supporting
the delayed or lazy computation of induction hypotheses,
mutual induction for conjectures about mutually recursive operations
as well as multiple complete or incomplete proof attempts
for the same conjecture.
The second part of this thesis deals with
as a software system.
We sketch the software architecture and describe the functionality of the system
(which can be utilized through a command interpreter or a graphical user interface).
The focus of the second part,
is on the approach to the problem of proof control
This approach is based on so-called (proof) tactics,
i.e. proof control routines written in a special proof
control language named QML.
as part of the approach,
a set of tactics (in addition to the elementary inference rules),
which range from tactics for trivial simplification steps to tactics
representing comprehensive inductive proof procedures.
Moreover, the system allows new tactics (written by the user in QML)
to be integrated into the system to enhance its performance.
we supply experimental evidence for our claim
that the desired (partial) automation of the proof control of
has been achieved to a considerable extent.