Selecting appropriate induction cases is one of the major problems in proof by induction. Heuristic strategies often use the recursive pattern of definitions and lemmas in making these selections. In this paper, we describe a general framework, based upon unification, that encourages and supports the use of such heuristic strategies within a Z-based proof system. The framework is general in that it is not bound to any particular selection strategies and does not rely on conjectures being in a "normal form" such as equations. We illustrate its generality with proofs using different strategies, including a simultaneous proof of two theorems concerning mutually-defined relations; these theorems are expressed in a non-equational form, involving both universal and existential quantifiers.
展开▼
