Rewrite-Based Inductive Theorem Proving
Our research activities have their origins in the D4-Project
(Reasoning in Equationally Defined Structures) which was funded within the
former Sonderforschungsbereich 314.
Throughout the last few years our overall goal has been the design and
implementation of a rewrite-based first-order inductive theorem prover.
As to the prover's main application area we intend to use it
for the (algebraic) specification of and formal reasoning about data types
such as the natural numbers, lists, strings, graphs etc.
The formal basis of our inductive theorem proving system QuodLibet
is given by a logical framework for inductive theorem proving (ITP)
that essentially consists of a specification language
for the formalization of data types, a calculus for inductive proofs
and so-called proof state graphs as a means of representing
the various kinds of dependencies among formulas in proofs.
Requirements with regard to our framework for ITP
In January 1997, we completed version 1.0 of QuodLibet,
our inductive theorem proving system.
In this version, QuodLibet presents itself as a mere proof
checker that facilitates interactive constructions of induction
However, this version offers a sophisiticated graphical user interface
allowing the visualization of proof processes.
- Data types with partial operations:
Our constructor-based specification language admits positive/negative
conditional rewrite rules as defining axioms for the operations of the
data type to be formalized. As to the semantics of specifications,
the model class we suggest is particularly well-suited for modelling data
types with partial operations which often lead to incomplete or even
non-terminating specifications. Furthermore, the admissibility
conditions of our specification language do not presuppose
termination and can often be effectively verified.
Experience shows that proving non-trivial inductive theorems with an
inductive theorem prover normally involves a knowledgeable user
who may have to interact with the prover in various ways. For that purpose,
it is often crucial that the user can achieve a good understanding of
the state of the current (possibly failed) proof attempt.
This can be facilitated by providing a calculus for
inductive proofs that is oriented towards human proof techniques
and easily comprehensible to the user.
Besides, proving within our framework is goal-directed
and there is a concept for the explicit representation of (partial)
derivations and proofs in a form suited to the user's needs.
For the successful construction of sophisticated proofs with an inductive
theorem prover, it may be necessary for the user to be able to translate
his hand-made proof sketches into concrete inference steps and make the
prover execute these. Therefore, our calculus for inductive proofs also
comprehends certain expressive inference rules that formalize
important human proof techniques but lead to infinite branching points in
the search space. Examples of such inference rules are rules for case
analyses or explicit instantiations of lemmas and induction hypotheses.
Nevertheless, we believe that to be acceptable to most users, an inductive
theorem prover needs to be capable of proving simple theorems without user
intervention. In order to facilitate the (partial) automation of finding
proofs in our framework we place important restrictions on the
specification language and the representation of inductive theorems:
Neither higher-order variables nor predicate symbols (except for `=')
nor explicitly quantified formulas will be admitted;
and we also restrict axioms and inductive theorems to (equational) clause
Currently, we are extending QuodLibet with a proof guidance component
that is intended to (partially) automate the construction of proofs.
This component is based on QML (QuodLibet Meta
Language), a language that allows the user to formulate proof tactics
relative to the inference machine of QuodLibet.
QML-tactics can be compiled and loaded into the system
to provide higher-level rules of inference or even complete proof strategies.
- Kühler, U.; Wirth, C.-P.: Inductive Theorem Proving in Theories
Specified by Positive/Negative-Conditional Equations, SEKI Report
SR-95-15, University of Kaiserslautern, 1995.
- Kühler, U.; Wirth, C.-P.: Conditional Equational Specifications
of Data Types with Partial Operations for Inductive Theorem Proving,
Proc. RTA-97, LNCS 1232, 1997, pp.38-52.
Extended Version as SEKI-Report SR-96-11, University of Kaiserslautern,
If you have questions, problems or suggestions send email to