Accession Number : ADA258660
Title : Quantification in Nqthm: A Recognizer and Some Constructive Implementations
Descriptive Note : Technical rept.
Corporate Author : COMPUTATIONAL LOGIC INC AUSTIN TX
Personal Author(s) : Kaufmann, Matt
Report Date : Aug 1992
Pagination or Media Count : 27
Abstract : We present an implementation of a recognizer for quantified notions in the Boyer-Moore Theorem Prover, Nqthm. That is, we provide a method for checking that a given function does indeed represent a quantified notion. We also present methods for generating constructively-presented functions that represent quantified notions, including definitions using only bounded quantifiers.
Descriptors : *COMPUTER PROGRAMMING , *THEOREMS
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE