Generalization in the Presence of Free Variables: a Mechanically-CheckedCorrectness Proof for One Algorithm

摘要

In this paper we present a mechanically-checked proof of correctness for ageneralization 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)