5.1 Installation instructions

In this section, we explain how to install MacLogic on your Apple Macintosh and how to customise it for your own (or your students') use. Some difficulties may arise, for example with memory management: if you experience these, and the information below fails to help you to sort out the problems, contact those responsible for maintaining the software by e-mail to the address at the end of this manual.

5.1.1 System requirements
5.1.1.1 Hardware and system software

MacLogic 3 works under system 7 (and later), but without exploiting the special features thereof such as "Balloon Help". An older version, 2.5, runs under system 6, but is no longer supported.

If installing from a floppy disc, ensure that your MacLogic disc is write-protected. Copy all the files from your MacLogic disc to either a hard or a floppy disc, and put your MacLogic disc in a safe place.

A machine to run MacLogic under system 7 (or later) MacLogic requires at least 4Mby of RAM, and prefers 8 MBy of RAM.

If there is not enough free RAM in your Macintosh, MacLogic may either fail to load, or will load improperly and not be of any use. It may even load partially, but not have a File menu allowing you to quit gracefully: in this case, you have to reboot your Macintosh via the "reset switch": for details of this procedure, see your Macintosh manual.

5.1.1.2 Installing the logic fonts

The disc or web site on which MacLogic is supplied contains a folder "Fonts for MacLogic". This contains

  1. a suitcase file called "Detroit Fonts", containing a 12 pt bit-mapped font Detroit, for the menus and dialogs. Detroit is based on Chicago, with extra characters for the logic symbols. Its font ID is 149.
  2. versions of the Konstanz font. Konstanz is based on Geneva, with the same extra characters as Detroit. Its font ID is 2500. It is available as 9 and 12 pt bit-maps in a suitcase, in TrueType format and in PostScript Type 1 format. At least install the bit-maps; install the others if you want to print MacLogic documents (or this documentation).

For best results, these two fonts should be installed in your System folder. To do this, see your Macintosh manual for details. Begin by discarding all old versions of Konstanz and Detroit in your system file. (If you must, keep copies in a safe place.) Older versions of MacLogic had the fonts attached to the application MacLogic itself: this still works fairly well, but the recommended method now is to install the fonts in your System folder.

Once the fonts are installed, you can of course use them while writing your logic essays with a word processor.

5.1.1.3 Memory management

Older versions of MacLogic allowed you to change the evaluation space etc used by the underlying MacProlog engine. This is no longer possible, except with great difficulty. All you can do is changethe memory allocation in the Finder to as much as you like. 2.8Mby is the minimum allowed. 4Mby is the minimum recommended.

5.1.2 What files are needed, where

MacLogic is distributed as a demonstration version. Details of how to upgrade it to a full working version are available to licence holders.

The code file necessary for MacLogic to work is

There are some help files, without which the on-line help system will not be usable. These live in a folder called HELP, and are called:

See section 5.1.3.2 below for details of how these help files can be edited.

At the time of writing, it is intended to replace these by a web-based Help system--- part of this documentation.

The application MacLogic should be kept in a folder, which should also contain the HELP folder. Do not drag MacLogic onto the desktop and then try to run it: when it comes to looking for the HELP folder, it expects to find it in the same folder as itself. Leave it in its own folder! You can of course create an alias and put that on the desktop, or in the Apple Menu folder.

There is also a folder of fonts:

As noted above, some of the contents of this folder must be installed in your system file before you use MacLogic or even view the documentation.

The following additional files may be available:

but, if not available, they can be generated easily when you run MacLogic.

5.1.3 Customisation instructions

MacLogic can be customised for your own (or your students') use in various ways. You can create a file "MacLogic Settings" which records the state of all the options in most of the menus for example if you always prefer to use Construct mode and Classical Logic, and to have your windows in 9pt. You can also edit the help files, if you don't like the way in which the rules etc are explained. You can build libraries of problems of your own. You can save theorems for use with the rule "Sequent Introduction". How to do all this is described below.

5.1.3.1 MacLogic Settings

When MacLogic is being loaded, it looks for a file "MacLogic Settings" in its home folder. The file should contain some code (in Prolog) recording how the various menu options were set when it was last modified. If it doesn't find it there, it will look in the Preferences folder inside the System folder. This file can be of type TEXT, or of type SRN1; in the latter case, it must have been created by MacLogic, i.e. its creator must be MALT.

If the file is present, and is of the right type, the contents are interpreted and the menu settings of MacLogic are reset accordingly.

You may at any tme also load menu settings from a file, of any name, provided that it is of type SRNB and was created by MacLogic.

You may save settings files: the file is given the type SRNB, identifying it as a Settings file. An earlier version of MacLogic prompted you to save settings if they had changed: this feature has been removed. You can name it "MacLogic Settings" and put it where it will be loaded automatically (see above).

Note that the correct name is NOT "MacLogic settings" or "Maclogic Settings".)

(It is not necessary to know anything about Prolog to be able to create or use this file.)

5.1.3.2 Changing the Help information

The HELP folder contains several help files, which you are free to edit. Note the format carefully: only edit the bits in between the comment marks /* and */. Save them as TEXT documents if you use a word processor to do the editing. The best way is to use MacLogic itself as a text editor, and then the files are saved as TEXT documents automatically. Ensure that your new versions have the correct names (as in section 5.1.2 above), with the correct upper case/lower case distinctions. When saving from MacLogic you will have to use new names like "New Tactics Help" for a while.

5.1.3.3 Building and editing problem libraries

MacLogic comes with a standard library of problems, called "MacLogic Problems". This is pre-loaded automatically, if it is kept in the home folder, when MacLogic is loaded. You can create similar problem libraries for yourself.

Library files are of two kinds: textual and coded. The textual form is in case you want to edit or print it with a word-processor, in which case use just the Konstanz font. The coded form is for speed of use by MacLogic. MacLogic can convert between the two forms for you.

The format of the textual form is a sequence of lines containing problems. A problem is

Any part of a line including and following a % symbol is ignored, so you can include comments of your own. Blank lines are ignored. Note that a problem must fit on a single line, as indicated by the Carriage Return character rather than the visual appearance. If a problem is being read for storage in the library, there is a restriction of its being at most 255 characters long. (Larger problems can be tackled by MacLogic, e.g. if typed in the Jotter window, so long as the formulae don't exceed 255 characters; but they can't be put in the library.)

To create a library file from scratch, use the Create... command from the Windows menu of MacLogic, and choose a name such as "My Library" for the new window. Type or paste the problems into the window in the format just described. You can check as you go along that each problem is syntactically correct, and even whether or not it is solvable, by using the standard features of MacLogic, such as Front window from the Problem menu. Save the file, using the Save to text file... item in the File menu.

Leave the window as the front window. To convert it to a coded form, use the command Load library problems from the File menu, and select the option of loading from the front window. The window will be read by MacLogic, and the information stored in memory, for immediate use. This takes some time, since the problems you have typed have to be parsed (i.e. converted from textual to coded form). Hopefully you checked them all for syntax errors as you typed them in. Now use Save library problems from the File menu, and save to a new coded file, such as "My Library Coded". You may wish to rename this later to "MacLogic Problems", having first put the old file of that name in a safe place; then you can arrange, as above, for it to be loaded automatically. The type of the file is 'SRN2'.

To edit an existing library file, the method depends on whether it is textual or coded. If it is textual, open it as a text file (Open text file... from the File menu), then edit it, and save it as a text file. (The steps just described above can be used to parse it into a coded form suitable for future use.) If it is coded, first load it into the library (Load library problems from the File menu), save it as a text file, and then proceed as above.

Library files can of course be printed. Text files can be loaded, as just described, and then printed (Print visible windows... from the File menu.) Coded files can be loaded into memory (Load library problems from the File menu), then saved to a text file (Save library problems from the File menu), then loaded into a window and printed as just described.

The folder "Problem files" contains several examples of libraries, all in textual form. Some are routine problems: some are rather hard. Some are unsolvable, being used for testing the automatic theorem proving facilities.

5.1.3.4 Building theorem files

When you use MacLogic, it is often convenient to appeal to a theorem proved earlier by solving a problem. So, as you solve problems, you may wish to keep them as theorems for future use. This is done by ensuring that the item Keeping as theorem in the Options menu is ticked. All zero-order problems that you solve will then be remembered, provided you give them names when prompted to do so. There is a minor restriction on the syntax alllowed in the name, clear from the dialog.

On loading MacLogic, if a file "MacLogic Theorems", of the right type (SRNB) and with the right contents, is in the folder to which MacLogic belongs, then it is loaded as a database of theorems.

If you wish to prove lots of theorems rather fast, create a library containing them all as problems, ensure that Keeping as theorem is ticked on the Options menu, and use the automatic mode to solve all the problems one by one, naming them as you go along. Note that you can select a problem in the front window and then choose Front window from the Problem menu rather than entering the problem into a dialog.

Better still: find an item in the Problem menu called Test run: if you select this, it attempts to solve all the problems in the library, reporting in the Jotter window the time taken for each problem. However, if your theorems are in different logics, this will be inconvenient, and you'll have to get them proved one by one, adjusting the logic each time to the most primitive logic in which the result is provable.

5.1.3.5 Foreign language environments

There is no convenient way of customising MacLogic to work in a language other than English. You can edit the help files, but the dialogs are not editable, being not stored as resources but as Prolog code.

If your Macintosh is organised for languages other than English, it may be necessary to work out what keystrokes are needed for the different logical symbols. This should be obvious from KeyCaps or (better) a utility like KeyFinder or PopChar. Information about the Syntax is available from the Help/Syntax menu item or in the file "Syntax Help", but the assignment therein of keystrokes to special symbols will have to be worked out for your keyboard. It is probably best to use the information in the Advice window (or the Help about Syntax) to get ASCII keystroke equivalents.

In case all else fails, here are the ASCII codes for the interesting symbols:

MacLogic works best with a British keyboard.