Abstract notions and inference systems for proofs by mathematical induction

Abstract

Soundness of inference systems for inductive proofs is sometimes shown ad hoc and a posteriori, lacking modularization and interface notions. As a consequence, these soundness proofs tend to be clumsy, difficult to understand and maintain, and error prone with difficult to localize errors. Furthermore, common properties of the inference rules are often hidden, and the comparison with similar systems is difficult. To overcome these problems we propose to develop soundness proofs systematically by presenting an abstract frame inference system a priori and then to design each concrete inference rule locally as a sub-rule of some frame inference rule and to show its soundness by a small local proof establishing this sub-rule relationship. We present a frame inference system and two approaches to show its soundness, discuss an alternative, and briefly classify the literature. In an appendix we give an example and briefly discuss failure recognition and refutational completeness.