MacLogic is a proof assistant for first-order logic on the Apple Macintosh.

MacLogic was developed specifically for the Apple Macintosh, which has consistently had an excellent user interface. If you want a similar tool for another kind of computer, please look elsewhere:

- a logic software list run by the American Philosophical Association
- the logic part of the resources guide of the Computers in Teaching Initiative at Oxford University
- Logic Software and Logic Education (at Groningen University)

MacLogic is intended for use as a tool in the teaching of systems of natural deduction in elementary logic. It is based on the work of Gentzen. It incorporates two modes for proof construction: top-down and bottom-up. It includes automatic theorem-provers, which can be used to indicate when a trial proof construction will fail. From December 1994, there are two versions:

- MacLogic 2 (in case you have modest amounts of RAM in your Macintosh or are using System 6)
- MacLogic 3 (in case you are using System 7 and 32-bit addressing on your Macintosh)

MacLogic is a product of the MALT (Machine Assisted Logic Teaching) project at St Andrews University. An earlier version won the 1988-89 Philosophy Software Contest arranged by the Philosophy Documentation Centre, Bowling Green State Univ., Ohio.

- On-line Help about all menu items, rules, tactics, syntax, ...; Help files can be edited.
- Manual of 76 pages, including a "Getting Started" section aimed at beginners.
- Fonts (such as our TrueType/Postscript font "Konstanz", based on "Geneva") incorporating the logical constants for negation, disjunction, conjunction, implication, bi-implication, absurdity, negation, possibility, necessity, strict implication and the two quantifiers. These fonts also contains Girard's symbols for linear logic, for use in our other program MacLL (freely available by FTP or WWW but unsupported).
- Window system for opening, editing and saving text files, making notes, constructing files of problems. Problem files can easily be created for student use.
- Check mode, for use in the traditional way as a checker of a (natural deduction) proof, entered line-by-line from the assumptions to the conclusion, allowing backtracking and with a wide range of error messages.
- Construct mode, based on the sequent calculus LJ, for use in top-down construction of proofs. Allows backtracking; wide range of error messages.
- Theorems proved may be saved (in present version, only if zero-order) for future use. All proofs are displayed and can be saved as text files.
- Various logics are implemented: minimal, intuitionistic, or classical propositional and predicate calculi, with or without equality, with or without rules for the modal logics S4 and S5. [Compound terms, like f(x)+y, are not supported.]
- Alpha-convertibility can be either enabled or disabled. When it is enabled, formulae differing only in the names of their bound variables are regarded as identical.
- Automatic theorem-provers can be used to check problems for solvability, and thus to warn about attempts to solve insolvable (sub-)problems. (Not yet for modal logic.)

MacLogic is based on the view that one should provide tools not just to allow students to check proofs that they have already discovered, but to help them with the more interesting art of constructing proofs.

It recognises that there are different logical systems, but in the interests of clarity adopts just one, essentially due to Gentzen, in which the meanings of the logical constants are as given by their introduction and elimination rules. Thus, classical logic is seen as the variant of intuitionistic logic in which one also has the rule of double negation, and minimal logic as the variant where one omits the rule of Absurdity elimination.

Proofs may be constructed in the top-down mode (Construct mode), using Gentzen's sequent calculus LJ; these are then translated mechanically, as described by Prawitz, to natural deduction proofs, laid out in the linear style of Lemmon's text. (Proofs may also be entered line-by-line in this style.)

The user interface is based on the standard facilities provided on the Apple Macintosh: mouse input to select menu items and dialog buttons, windows, scroll-bars, scrolling menus, high-resolution graphics. Especially in Construct mode, little typing is required. (Those wanting to type lots of formulae can of course do so, in Check mode.)

- MacLogic 2:
- Application size about 540K, preferred RAM requirement 1000K, Multifinder and System 7 compatible. Recommended for use on any Macintosh without 32-bit addressing or not using System 7. Works under System 6.0.7 and some earlier systems. Not suitable for use on machines using 32-bit mode (e.g. to address large amounts of RAM).
- MacLogic 3:
- Application size about 800K, preferred RAM requirement 3500K, needs System 7. Recommended for use on any Macintosh with 32-bit addressing (e.g. PowerPC-based machines, Quadras in 32-bit mode, etc).

The British rather than the US keyboard is preferred: it can be used with the latter, but not quite so conveniently, e.g. the symbol for the Universal quantifier is option-shift U in Britain but something less memorable in the US. From version 3.0.3, combinations like \A can be used for the universal quantifier, etc.

- Notices of the American Math. Soc. (February 1993)
- Computer Journal 36 (4), pp 373-386 (1993) (long version of (1))
- American Philosophical Association Newsletter (Autumn 1993)

No specific textbook accompanies MacLogic.

The book "Modern Logic", by Graeme Forbes, Oxford University Press 1994, (ISBN 0-19-508029-7) was written for use in conjunction with MacLogic.

The latest version (a rather restrictive demo version) is always available free of charge. It can be obtained in various ways:

- From the world-wide web, look at my home page, with URL "http://www-theory.dcs.st-and.ac.uk/~rd/" and follow the obvious links and instructions.
- By anonymous FTP from ftp.dcs.st-andrews.ac.uk, directory pub/malt
- If you use Eudora on your Macintosh, I can mail you the files.

Those who ask are told how to convert the demo version to the full version.

Dr Roy Dyckhoff,Computer Science Division, The University, St Andrews, Fife, KY16 9SS, Scotland.

rd@dcs.st-andrews.ac.uk