
Accession Number : ADA006898
Title : FOL: A Proof Checker for Firstorder 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 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 : *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