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
- 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!
- 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:
- 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.
- 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.
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
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.
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
- 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
- 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,
- MacLogic 3.0 (22/12/94) was based on the 32 bit clean reimplementation
- 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.
Roy Dyckhoff, 5 April 2006