A Proof Assistant for First-Order Logic on the Macintosh

MacLogic is a proof assistant for first-order classical, intuitionistic and minimal logic, with or without equality, and either non-modal or modal (S4 or S5). It runs on any Apple Macintosh with at least 2 Mbyte RAM (an old version for 1Mby is available on request.) It works in two modes: as a proof checker and as a proof constructor. The proof checker verifies that a proof is indeed correct by checking it line by line in a "bottom-up" fashion. Proofs are laid out in the style of E. J. Lemmon's Beginning Logic. However, the rules are not Lemmon's, but much closer to Gentzen's original natural deduction systems NK, NJ and NM. The proof constructor uses a "top-down" approach, based essentially on Gentzen's sequent calculi such as LJ: once a proof has been constructed, it is transformed mechanically into one laid out in Lemmon's style:

Problems may be entered by the user, read from a library file or read from a window on the screen. Complete proofs can be saved to disc and can be printed out either from within MacLogic itself, or by using any word-processor. Complete proofs can also be saved to a window: previous proofs from the current session can thus be inspected. Solved propositional problems may be kept as theorems for later use, during either the same or a later run of MacLogic.

Windows can be created, edited, saved, printed and killed as usual. They can be used for editing problems, constructing libraries of problems, or just making notes. So, MacLogic can be used as a text editor.

Theorem provers for various logics are included, to warn about attempts at unsolvable problems. They can be switched off if obtrusive.

An extensive on-line Help system reduces the need for availability of a manual beside the computer.

A special font, Konstanz, including a wide range of logical constants in addition to the standard Geneva character set, is included, both in bit-map form and in TrueType and PostScript type 1 format.