A Theorem-Prover for Recursive Functions: A User's Manual.

Abstract

A user's manual for an automatic theorem-proving computer program is presented. We here describe how to use the program, which is written in the INTERLISP dialect of LISP. Matters covered include our syntactic conventions; starting up the theorem-prover; defining functions; proving and storing lemmas; undoing previous work; and examining and saving the theorem-prover's state. More than 30 user commands are defined and described. Simple examples are given.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1979
Accession Number
ADA070905

Entities

People

  • J. Strother Moore
  • Robert S. Boyer

Organizations

  • SRI International

Tags

Communities of Interest

  • Advanced Electronics
  • Space

DTIC Thesaurus Topics

  • Computer Program Verification
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Databases
  • Directories
  • Language
  • Military Research
  • New York
  • Operating Systems
  • Procedures (Computers)
  • Programming Languages
  • Recursive Functions
  • Standards
  • United States
  • United States Government

Readers

  • Computational Linguistics
  • Computer Science.
  • Mathematical Modeling and Probability Theory.