Report Number: CS-TR-76-572
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/76/572/CS-TR-76-572.pdf