Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

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

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.
User-orientation: 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.
Expressiveness: 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.
Automation: 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 form.

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.

Availability:

Version 1.3 is available for download. Please read the installation instructions.
Version 1.2 is available for download. Please read the installation instructions.
Version 1.1 is available for download. Please read the installation instructions.

Case Studies:

sortalgos: Sorting algorithms (insertion sort, merge sort, quick sort, bubble sort)
gcd: Properties of gcd (e.g. Associativity)
sqrt2-hippasos: Irrationality of sqrt(2) based on ideas of Hippasos of Metapont
sqrt2-euclid: Irrationality of sqrt(2) based on ideas of Euclid of Alexandria
lpo: Properties of LPO (e.g. simplification order)
exp-exhelp: Equivalence of call-by-value and call-by-name evaluations for simple arithmetic expressions containing function calls

Persons Involved:

Publications:

Schmidt-Samoa, T.: The new standard tactics of the inductive theorem prover QuodLibet, SEKI Report SR-2004-01, Universität des Saarlandes, 2004.
- Download full paper (97 Kbytes)
Avenhaus, J.; Kühler, U.; Schmidt-Samoa, T.; Wirth, C.-P.: How to Prove Inductive Theorems? QuodLibet!, 19th CADE, LNAI 2741, pp. 328-333, Springer, 2003.
- Download full paper (97 Kbytes)
- Copyright Owner: Springer
Wirth, C.-P.: Descente Infinie + Deduction, Report 737/2000, FB Informatik, Univ. Dortmund. Journal Version.
Kühler, U.: A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations, Ph.D. Thesis, University of Kaiserslautern, 2000, Infix, Sankt Augustin.
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, 1996.
- Abstract
- Download full paper (97 Kbytes)
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.
- Abstract
- Download full paper (301 Kbytes)
Wirth, C.-P.; Gramlich, B.: A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications, J. Symbolic Computation 17, 1994, pp.51-90, Academic Press.
Wirth, C.-P.; Gramlich, B.: On Notions of Inductive Validity for First-Order Equational Clauses, 12th CADE 1994, LNAI 814, pp. 162--176, Springer. The Paper is available at Claus-Peter Wirth's homepage.

Internal Papers

Rondot, R.: Integration von Entscheidungsverfahren in den induktiven Theorembeweiser QuodLibet, Diplomarbeit (German), Fachbereich Informatik, Technical University of Kaiserslautern, Germany, 2004.
- Download full paper (344 Kbytes)
Kaiser, M.: Effizientes Beweisen mit einem formalen Beweissystem, Diplomarbeit (German), Fachbereich Mathematik, University of Kaiserslautern, Germany, 2002.
- Download full paper (640 Kbytes)
Kühler, U.; Embacher, C.; Eschbach, R.; Schumacher, J.; Schmidt-Samoa, T.; Sprenger, C.: QuodLibet. System-Dokumentation (German), Fachbereich Informatik, University of Kaiserslautern, Germany, 1998.
- Download full paper (100 Kbytes)
Schumacher, J.; Kühler, U.: XQL - a graphical user interface for the inductive theorem prover QuodLibet, Unpublished technical report, Fachbereich Informatik, University of Kaiserslautern, Germany, 1997.
- Download full paper (124 Kbytes)
Schmidt-Samoa, T.: Realisierung einer Taktik-basierten Beweissteuerungskomponente für den induktiven Theorembeweiser QuodLibet, Projektarbeit (German), Fachbereich Informatik, University of Kaiserslautern, Germany, 1997.
- Download full paper (224 Kbytes)
Sprenger, C.: Über die Beweissteuerung des induktiven Theorembeweisers QuodLibet, Diplomarbeit (German), Fachbereich Informatik, University of Kaiserslautern, Germany, 1996.
- Download full paper (188 Kbytes)
Embacher, C.: Entwurf und Implementierung eines prototypischen Induktionsbeweisers für positiv/negativ bedingte Rewrite-Spezifikationen - eine softwaretechnische Realisierung, Projektarbeit (German), Fachbereich Informatik, University of Kaiserslautern, Germany, 1995.
- Download full paper (204 Kbytes)

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

Letzte Änderung: Wednesday, 26-Oct-05 08:59:21 GMT
www-aven@informatik.uni-kl.de

Formale Methoden und Deduktion Prof. Dr. J. Avenhaus