Accession Number : ADA006898

Title :   FOL: A Proof Checker for First-order Logic

Descriptive Note : Technical rept.

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Weyhrauch, Richard W ; Thomas, Arthur J

PDF Url : ADA006898

Report Date : Sep 1974

Pagination or Media Count : 63

Abstract : This manual describes the use of the interactive proof checker FOL. FOL implements a version of the system of natural deduction described by Prawitz, augmented in the following ways: (1) it is a many-sorted first-order logic and a partial order over sorts may be declared: this reduces the size of formulas; (2) purely propositional deductions can be made in a single step; (3) the truth values of assertions involving numerical and LISP constants can be derived by computation; (4) there is a limited ability to make metamathematical arguments; and (5) there are many operational conveniences. The goal of FOL is to use formal proof techniques as practical tools for checking proofs in pure mathematics and proofs of the correctness of programs. It is also intended to be used as a research tool in modelling common-sense reasoning in the representation theory of artificial intelligence.

Descriptors :   *ARTIFICIAL INTELLIGENCE, *COMPUTER APPLICATIONS, *MATHEMATICAL LOGIC, BOOLEAN ALGEBRA, COMPUTATIONS, COMPUTER PROGRAMMING, PROBLEM SOLVING, REASONING, SEMANTICS, SET THEORY

Subject Categories : Computer Programming and Software
      Bionics

Distribution Statement : APPROVED FOR PUBLIC RELEASE