Macintosh Software for Logic

See Branden Fitelsen's web site if you are using a modern version of MacOS (e.g. OS X) or are not a Macintosh user.

This software has been developed within the Computational Logic research group at St Andrews University, by Roy Dyckhoff, Neil Leslie, Tom Peillon, Brenda Rapley, Luis Pinto, Andrew Adams, Christian Urban, Jacob Howe and others.

It is copyright of the University of St Andrews.

You may need to use a utility such as BinHex or Stuffit Expander to unpack this software: if so, it'll probably end up in your system folder. It was packed using Compact Pro.

The demonstration versions of MacLogic listed below can be converted quickly into fully licensed versions.

• Introductory woffle about MacLogics: click here.
• Fonts for MacLogic: click here: download to get bitmap (9 and 12 pt), TrueType and Postscript versions of the Konstanz font, based on Geneva with lots of logical symbols, and the 12pt bitmap font Detroit (based on Chicago, with the same logical symbols as Konstanz). They come with a short README file about installation.

• proof assistant for various first-order logics, using both natural deduction and sequent calculus
• runs on Apple Macintosh under systems 6 and 7, but is not 32-bit clean.
• To download the demo version (350K BinHexed Compressed file), click here: download.
• MacLogic 2 documentation (Microsoft Word 4 file): click here: download. Install the fonts before trying to read or print it!

MacLogic 3.*

• proof assistant like MacLogic 2, is 32-bit clean, so will run on all Macintoshes (including PowerMacintosh, in emulation mode, and 32-bit addressed Quadras) with at least 6 Mby of RAM (for MacLogic). Needs System 7 or 8. The version number is below. To download the demo version (BinHexed Compressed files), click here:
  • download the application (600K)
  • download other files (HELP, Problem files, README) (54K)
  • Put the application in the folder "MacLogic f" got by the second download.
• MacLogic 3 documentation: this is a web site. Install the fonts first! You can download it all at once (217K) and (using a browser such as Netscape Navigator 4 that understand font tags) view it on a machine even without an internet connection. It will change as I update MacLogic and remove references to historical relics.

MacLL

• proof assistant for linear logics, developed by Thomas Peillon as an MSC project. To download MacLL (256K), click here: download. There is no charge; it needs the fonts for MacLogic (see above); it is unsupported. It is not 32-bit clean.

---

Warning

There are problems with some Macintoshes using OS 9 that I don't know how to fix; (and probably don't have the resources to fix even if I did know how to). See the above note about using MacLogic on non-Macintoshes.

Accordingly, we are no longer charging for MacLogic.

---

Pricing and ordering

• Demo version is free.
• Full version: no longer charged for, but email to RD first will get you the details of how to convert the demo version.

---

Version changes:

• MacLogic 3.4.1(26/10/99) fixed the bug that Settings files were not correctly loaded at startup in some circumstances.
• Documentation and HELP files updated slightly (23/10/99).
• The "other files" had the old coded problem file removed and replaced by one in the new format (23/10/99).
• MacLogic 3 documentation (9/9/99) was reorganised as a web site.
• MacLogic 3.4 (17/9/99) fixed some bugs concerning the HELP system and restored the MacLogic 2 features whereby Settings, Problems and Theorems can be saved and loaded:
  • Don't expect old settings files etc to work:: make up new ones if necessary.
  • Some of the HELP information is now a bit out of date :-).
• MacLogic 3.3 (9/9/99) fixed some long-standing problems with the display of the Detroit font.
• MacLogic 3.2 added code based on implementation of fast decision procedures for propositional intuitionistic and minimal logics.
• MacLogic 3.1 .. (I can't remember).
• MacLogic 3.0.1 (29/12/95) included a feature for Graeme Forbes, see page 359 of his "Modern Logic", Oxford UP 1994, for details)
• MacLogic 3.0 (22/12/94) was based on the 32 bit clean reimplementation of MacProlog.
• MacLogic 2.5 (9/1/95) is the final non-32-bit clean version, suitable for use on old small Macintoshes. It will not be developed any further. It has some features not yet implemented in versions 3.1-3.3, such as the loading and saving of theorems.