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


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a258660.pdf


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