Generalization in the Presence of Free Variables: a Mechanically-Checked Correctness Proof for One Algorithm
Abstract
In this paper we present a mechanically-checked proof of correctness for a generalization algorithm. Although the theorem itself is probably new (at least, we are unaware of any existing statement of it), the interest here lies not particularly in the theorem per se but, rather, lies in the demonstration of the use of mechanical verification for assisting the reliability of detailed proofs and software. In particular, we believe that this exercise strongly suggests the feasibility of creating a verified version of PC-NQTHM, i.e. one which is proved correct in the Boyer-Moore theorem prover or in some successor of that system. Thus, this paper could be viewed as a contribution to the study of metatheoretically extensible systems. Some reports of research in this spirit can be found in works of Davis and Schwartz (6), Weyhrauch (18), Boyer and Moore (2), Shankar (16), Knoblock and Constable (14, 13), Howe (9), and Quaife (15). However, we also view this paper as an exposition which provides a rather detailed look at the practice of using the Boyer-Moore theorem prover and PC- NQTHM to proof-check mathematical arguments. (kr)
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1990
- Accession Number
- ADA222681
Entities
People
- Matt Kaufmann