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

Introduction

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:

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 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.

Features

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.)

User-friendliness

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.)

System requirements

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.

Reviews

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

Textbooks

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.

Ordering details

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:

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