TY - JOUR

T1 - A calculational approach to mathematical induction

AU - Doornbos, H.

AU - Backhouse, R.C.

AU - Woude, van der, J.C.S.P.

PY - 1997

Y1 - 1997

N2 - Several concise formulations of mathematical induction are presented and proved equivalent. The formulations are expressed in variable-free relation algebra and thus are in terms of relations only, without mentioning the related objects. It is shown that the induction principle in this form, when combined with the explicit use of Galois connections, lends itself very well for use in calculational proofs. Two non-trivial examples are presented. The first is a proof of Newman's lemma. The second is a calculation of a condition under which the union of two well-founded relations is well-founded. In both cases the calculations lead to generalisations of the known results. In the case of the latter example, one lemma generalises three different conditions

AB - Several concise formulations of mathematical induction are presented and proved equivalent. The formulations are expressed in variable-free relation algebra and thus are in terms of relations only, without mentioning the related objects. It is shown that the induction principle in this form, when combined with the explicit use of Galois connections, lends itself very well for use in calculational proofs. Two non-trivial examples are presented. The first is a proof of Newman's lemma. The second is a calculation of a condition under which the union of two well-founded relations is well-founded. In both cases the calculations lead to generalisations of the known results. In the case of the latter example, one lemma generalises three different conditions

U2 - 10.1016/S0304-3975(96)00154-5

DO - 10.1016/S0304-3975(96)00154-5

M3 - Article

SN - 0304-3975

VL - 179

SP - 103

EP - 135

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-2

ER -