A users manual for FOL.

[摘要] 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.

[学科分类] 计算机科学（综合）