Accession Number:

ADA231375

Title:

An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification

Descriptive Note:

Corporate Author:

COMPUTATIONAL LOGIC INC AUSTIN TX

Personal Author(s):

Report Date:

1991-01-01

Pagination or Media Count:

19.0

Abstract:

We describe an implementation of an extension to the Boyer-Moore Theorem Prover and logic that allows first-order quantification. The extension retains the capabilities of the Boyer-Moore system while allowing the increased flexibility in specification and proof that is provided by quantifiers. The idea is to Skolemize in an appropriate manner. We demonstrate the power of this approach by describing three successful proof-checking experiments using the system, each of which involves a theorem of set theory as translated into a first-order logic. We also demonstrate the soundness of our approach.

Descriptors:

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE