1. Introduction

MacLogic is a tool intended to be used by the student learning to construct proofs in elementary logic. It is not a traditional piece of computer-based learning software, assigning marks for good work and so on: it is more like a word-processor than like a typing tutor. It has a modest amount of intelligence with which to warn you about incorrect or unpromising approaches to problems. One of the fascinations of logic, however, is that there are unsolvable problems: thus, MacLogic is not always able to show you what to do next!

By using MacLogic carefully and sensibly you will be able to learn a good deal about a variety of first-order logics. This manual will show you how to use MacLogic, and provides reference information to which you may refer when the on-line Help system incorporated in MacLogic is inadequate. In many cases, however, this on-line Help will give you as much information as you need, and thus you should soon be able to put this manual back on your shelf.

MacLogic is not intended to be, or to replace, an introductory text-book on logic, explaining the motivation, the notation, etc. Unfortunately, few text books are geared to the kind of computer-based approach that we espouse. One possible text on logic which can be used alongside MacLogic is that by Read & Wright: (see the bibliography in section 4.5). Another is that by Graeme Forbes: see the same bibliography.