Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

FB Inf

How to Prove Inductive Theorems? QuodLibet!

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 proofs. However, this version offers a sophisiticated graphical user interface allowing the visualization of proof processes.

In version 1.1 we have extended 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. The tactics are automtically integrated into the graphical user interface. Version 1.1 contains some predefined tactics that free the user from tedious work and provide simple proof strategies.


Case Studies:

Persons Involved:


Internal Papers
If you have questions, problems or suggestions send email to Tobias Schmidt-Samoa

Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!

Letzte Änderung: Wednesday, 26-Oct-05 08:59:21 GMT