
Accession Number : ADA006898
Title : FOL: A Proof Checker for Firstorder Logic.
Descriptive Note : Technical rept.,
Corporate Author : STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
Personal Author(s) : Weyhrauch,Richard W. ; Thomas,Arthur J.
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 manysorted firstorder 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 commonsense reasoning in the representation theory of artificial intelligence.
Descriptors : *MATHEMATICAL LOGIC, *COMPUTER APPLICATIONS, *ARTIFICIAL INTELLIGENCE, COMPUTATIONS, REASONING, COMPUTER PROGRAMMING, SEMANTICS, PROBLEM SOLVING, SET THEORY, BOOLEAN ALGEBRA.
Subject Categories : Computer Programming and Software
Bionics
Distribution Statement : APPROVED FOR PUBLIC RELEASE