Accession Number:

ADA222681

Title:

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

Descriptive Note:

Technical rept.

Corporate Author:

COMPUTATIONAL LOGIC INC AUSTIN TX

Personal Author(s):

Report Date:

1990-04-01

Pagination or Media Count:

95.0

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

Subject Categories:

  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE