MacLogic is a proof assistant for first-order logic on the
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
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
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
- 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
- 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,
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
- 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.
Obtaining the demo version or upgrades
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
- 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
Dr Roy Dyckhoff,
Computer Science Division, The University, St Andrews, Fife, KY16