Mechanizing structural induction part I: Formal system

AbstractInductive methods are basic to program proving and this paper presents the formal part of a theorem-proving system for automating mildly complex proofs by structural induction. Its features are motivated by the pragmatics of proof finding. Its syntax includes a typed language and an induction rule using a lexicographic ordering based on a substructure ordering. The domain of interpretation is a many-sorted word algebra generated by the empty set. The carriers of the algebra are ordered and functions are defined by k-recursion over them. Finally, the soundness and the weak completeness of the system are proved. The main quality of the language is its system of types and its correspondingly general induction rule