A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations

Authors: Ulrich Kühler
Title: A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations
In: PhD thesis, ISBN 3-89838-238-9, Infix, Akademische Verlagsgesellschaft Aka GmbH, Berlin
Copyright Owner: Akademische Verlagsgesellschaft Aka GmbH, Berlin
Abstract: 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$. Therefore, 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 (named QuodLibet) which we have developed to attain two essential goals. Firstly, 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. Secondly, 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 QuodLibet 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. In particular, 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). Moreover, 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 QuodLibet 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, however, is on the approach to the problem of proof control developed for QuodLibet. This approach is based on so-called (proof) tactics, i.e. proof control routines written in a special proof control language named QML. QuodLibet provides, 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. Finally, we supply experimental evidence for our claim that the desired (partial) automation of the proof control of QuodLibet has been achieved to a considerable extent.