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. For more information, see AIM-235, the FOL manual.