A Computational Logic for Applicative Common Lisp

Abstract

This final report is provided to satisfy a contract deliverable. We summarize here our results in automated reasoning under this contract. The development of the Boyer-Moor 'Nqthm' theorem prover was supported in part for approximately 20 years by the Office of Naval Research. The long range objective of this research has been to enable programmers to produce software that is mathematically proven to meet its specifications by using mechanical theorem- proving programs that check proofs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1994
Accession Number
ADA283103

Entities

People

  • Bob Boyer
  • Joseph Moore
  • Matt Kaufmann

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Artificial Intelligence Computing
  • California
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Databases
  • Ground Zero
  • High Level Languages
  • Language
  • Lisp Programming Language
  • Machine Languages
  • Military Research
  • Numbers
  • Programming Languages
  • Software Development

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Government Contracting/Procurement.
  • Mathematical Modeling and Probability Theory.