FOL is a proof checker for first order logic, a machine implementation of an extended version of the system of natural deduction described by Prawitz. It is invoked with the monitor command R FOL. The FOL manual is AIM-235, and may be found in the document room. An introductory text for the use of FOL is the FOL primer, AIM-288. It is available online as the file FOLPRM.REF[AIM,DOC].