- Claus-Peter Wirth,
- Abstract Notions and Inference Systems for Proofs by Mathematical Induction
- 4th CTRS, LNCS 968, 1994, pp. 353-373, Springer.
- Soundness of inference systems for inductive proofs
shown ad hoc and a posteriori, lacking modularization and interface
As a consequence, these soundness proofs tend to be clumsy,
difficult to understand and maintain, and error prone with difficult to
common properties of the inference rules are
and the comparison with similar systems is difficult.
To overcome these problems we propose to develop soundness proofs
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
briefly discuss failure recognition and refutational completeness.
- Full paper
- .1 Mbytes
- .1 Mbytes
The fonts of this version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
- .2 Mbytes