Quantification in Nqthm: A Recognizer and Some Constructive Implementations

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1992
Accession Number
ADA258660

Entities

People

  • Matt Kaufmann

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Abstracts
  • Arithmetic
  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Computer Programming
  • Ground Zero
  • Lisp Programming Language
  • Military Research
  • New York
  • Recursive Functions
  • Specifications
  • Theory Of Computation
  • West Germany

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.
  • Speech Processing/Speech Recognition.