zbMATH — the first resource for mathematics

Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm. (English) Zbl 0723.68072
Summary: We present a case study in which an automated proof assistant was used to show the correctness of an algorithm. Specifically, we document the application of an extension of the Boyer-Moore theorem prover to the problem of verifying the correctness of an implementation of generalization, where the proof had surprisingly many details and a previous implementation contained an error. We attempt to provide sufficient detail so that the reader can gain a realistic impression of the nature of this exercise.

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
HOL; LISP; Nuprl
Full Text: DOI