Accession Number:

ADA070905

Title:

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

Descriptive Note:

Technical rept.,

Corporate Author:

SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB

Personal Author(s):

Report Date:

1979-06-01

Pagination or Media Count:

66.0

Abstract:

A users 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-provers state. More than 30 user commands are defined and described. Simple examples are given.

Subject Categories:

  • Numerical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE