×

zbMATH — the first resource for mathematics

Derivation and use of induction schemes in higher-order logic. (English) Zbl 0890.03005
Gunter, Elsa L. (ed.) et al., Theorem proving in higher order logics. 10th international conference, TPHOLs ’97. Murray Hill, NJ, USA. August 19–22, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1275, 275-290 (1997).
This article is concerned with the verification of functional programs (e.g., programs written in the programming language ML) by using higher-order inductive theorem proving.
The presented approach is based on using noetherian induction instead of structural induction. Given a function definition in ML, under suitable hypotheses, one can derive automatically its induction scheme, that is, an instance of the noetherian induction principle specialized for the given program. Then one can use this instance to prove properties about the program by interactive theorem proving in the HOL (Higher Order Logic) system. Other methods for this kind of problem are the one based on the computational logic of Boyer and Moore, and the one based on cover sets in term rewriting. For the latter, see: H. Zhang, D. Kapur and M. S. Krishnamoorthy, Lect. Notes Comput. Sci. 310, 162-181 (1988; Zbl 0657.68103).
For the entire collection see [Zbl 0870.00024].

MSC:
03B35 Mechanization of proofs and logical operations
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B15 Higher-order logic; type theory (MSC2010)
Software:
HOL; ML
PDF BibTeX Cite