 | ||||||||||
| ||||||||||
| ||||||||||
| HOME | ||||||||||
| ||||||||||
 |
||||||||||
FOL - The Original Papers
Version 0.001 2020-04-15
- Author:
- Richard Weyhrauch (IBUKI)
- Note:
- This is an original personal document of Richard Weyhrauch hosted by IBUKI at http://rww.ibuki.com . This document is not in the public domain. The copyright is held by him and anyone wanting to reprint it must get his permission in writing. This document was written while he was employed by IBUKI but on his own time at at his own expense.
Abstract
The papers listed below describe the computer system FOL as implemented at the Stanford Artificial Intelligence Lab in the 1970s. FOL was the name of a computer program implemented using the notions of First Order Logic as a guide. The notions of FOL are found in FOL summary and the origin of these ideas are found in FOL History.
1974 FOL: A proof checker for First Order Logic Richard W. Weyhrauch and Arthur J. Thomas AIM-235 and STAN CA 74-432 This was the first FOL manual. It contains a usage of the word 'context' on page 2. It is a clear description of the logic of FOL It includes many examples, including axiomatizations of ZF and GBN. 1976 An FOL primer Robert E, Filman and Weyhrauch, Richard W. AIM-228 and STAN-CS-TR-76-572 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. ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/76/572/CS-TR-76-572.pdf 1976 A Users Manual for FOL, Stanford AIM 235.1, 1977. AIM-235.1 and CS-TR-77-432.pdf This PDF was made in some very strange way. I believe it printed from an AI lab text file and then converted to PDF. This is the only explaination for the strange rendering of the fonts and the symbols used for quantifiers. The AI lab keyboards and printers had the logic symbols on them using an ad hoc encoding but the reports we produced were accurately typeset. I have not yet found a copy of the original as it will have much better topography. I will produce a PDF with images when I find one. Sorry. 1978 Prolegomena to a theory of mechanized formal reasoning AIM-315 and CS-TR-78-687.pdf the main AI lab report 1980 Artificial Intelligence 13 (1980):133-170 This is the published paper describing the FOL system. It is the most complete and has been reprinted nine times, but its typesetting lost some information (mostly metatheoretical).