Tactic-based inductive theorem prover for data types with partial operations (Diss., Univ. Kaiserslautern, 1999) (Q2726307)

The overall subject of this dissertation is how to bild a system that can prove corecteness properties of the programs in a functional programming language obtained as rewrite systems from conditional equations for abstract data types. The problems to solve are: fixing an expressive specification language, the choise of an adequate semantics, presenting a proof calculus consisting of inference rules, implementing a prover based on tactics, which the user can call interactively and providing a graphical user interface to support interactive proof attempts. In the first chapter, the author presents a formal framework for inductive theorem proving, including the specification language and inferences rules for representenging proof constructions. In the second chapter inductive theorem prover \textit{QuodLibet } is introduced, including command language, the proof control language QML, QML routines and inductive proof strategies. In Appendices A, B, C, D and E are presented the proofs, the syntax and the inferences rules for \textit{QuodLibet } and also syntax of QML and examples of proof constructions.NEWLINENEWLINEThe thesis can serve as instructional material for a course on theorem proving or AI at graduate level.