FOL(ID:3315/fol001)for First Order Logic Filman Stanford 1976 Places Related languages
References: Institution: Stanford University, Department of Computer Science Title: An FOL primer Author: Filman, Robert E. Author: Weyhrauch, Richard W. Date: September 1976 Abstract: This primer is an introduction to FOL, an interactive proof checker for first order logic. Its examples can be used to learn the FOL system, or read independently for a flavor of our style of interactive proof checking. Several example proofs are presented, successively increasing in the complexity of the FOL commands employed. pdf Institution: Stanford University, Department of Computer Science Title: A users manual for FOL. Author: Weyhrauch, Richard W. Date: July 1977 Abstract: This manual explains how to use of the proof checker FOL, and supersedes all previous manuals. FOL checks proofs of a natural deduction style formulation of first order functional calculus with equality augumented in the following ways: (i) it is a many-sorted first-order logic in which a partial order over the sorts may be specified; (ii) conditional expressions are allowed for forming terms (iii) axiom schemata with predicate and function parameters are allowed (iv) purely propositional deductions can be made in a single step; (v) a partial model of the language can be built in a LISP environment and some deductions can be made by direct computation in this model; (vi) there is a limited ability to make metamathematical arguments; (vii) there are many operational conveniences. A major goal of FOL is to create an environment where formal proofs can be carefully examined with the eventual aim of designing practical tools for manipulating proofs in pure mathematics and about the correctness of programs. This includes checking proofs generated by other programs. FOL is also a research tool in modeling common-sense reasoning including reasoning about knowledge and belief. pdf |