 Authors
 ClausPeter Wirth,
Klaus Becker
 Title
 Abstract Notions and Inference Systems for Proofs by Mathematical Induction
 In
 4th CTRS, LNCS 968, 1994, pp. 353373, Springer.
Bibtex Entry
 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 subrule
of some frame inference rule and to show its soundness by a small local
proof establishing this subrule 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.
 Full paper

 Format
 .ps.gz
 Size
 .1 Mbytes

 Format
 .dvi
 Size
 .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!
 Format
 .pdf
 Size
 .2 Mbytes