\newpage \begin{center} {\Large\bf CONTENTS} \end{center} \hugeskip \begin{tabbing} Major \= minor header \= \hs{100mm} \= p\kill {\bf I} \> INTRODUCTION \> \>\ 2 \\[3mm] {\bf II} \> INSTALLATION GUIDE \\[2mm] \> {\bf 2.1} \> Installing MaGIC \>\ 6 \\[3mm] \> {\bf 2.2} \> Installing Xmagic \>\ 9 \\[3mm] {\bf III} \> USER'S GUIDE TO MaGIC \\[2mm] \> {\bf 3.1} \> A MaGIC Tutorial \> 12 \\[3mm] \> {\bf 3.2} \> The Menu Options \> 18 \\[3mm] \> {\bf 3.3} \> The Ugly Data Format \> 26 \\[3mm] \> {\bf 3.4} \> An Xmagic Tutorial \> 29 \\[3mm] \> {\bf 3.5} \> Xmagic Reference Guide \> 32 \\[3mm] {\bf IV} \> MODELLING LOGIC \\[2mm] \> {\bf 4.1} \> Propositional Structures \> 36 \\[3mm] \> {\bf 4.2} \> Vocabulary \> 41 \\[3mm] \> {\bf 4.3} \> Some Postulates and Systems \> 43 \\[3mm] {\bf V} \> HOW IT WORKS \\[2mm] \> {\bf 5.1} \> Overview of the program \> 49 \\[3mm] \> {\bf 5.2} \> Generating and Testing Matrices \> 51 \\[3mm] \> {\bf 5.3} \> Transferred Refutations \> 56 \\[3mm] \> {\bf 5.4} \> Parallelisation \> 60 \\[3mm] {\bf VI} \> SOME PERFORMANCE DATA \\[2mm] \> {\bf 6.1} \> The C8 Benchmark \> 63 \\[3mm] \> {\bf 6.2} \> The R10 and R12 Benchmarks \> 65 \\[3mm] \> {\bf 6.3} \> The PW5 Benchmark \> 66 \end{tabbing} \newpage \begin{center} {\Large\bf I} \vspace{2mm} {\large\bf INTRODUCTION} \end{center} \vspace{15mm} The program MaGIC (Matrix Generator for Implication Connectives) is intended as a tool for logical research. It computes small algebras (normally with up to 14 elements) suitable for modelling certain non-classical logics. Along the way, it eliminates from the output any algebra isomorphic to one already generated, thus returning only one from each isomorphism class. Optionally, the user may specify a formula which is to be {\em invalid\/} in each structure found. This enables MaGIC to be used for such purposes as showing invalidity of unwanted formul\ae, proving one system stronger than another and proving the independence of axioms. It can also be used to generate all the small algebras modelling some chosen logic. These can then be used as input for other programs: for instance, they can be used as a database for many purposes including those of refuting non-theorems. They can also be presented in a human-readable format so that they may be perused, for example to suggest metatheorems to an imaginative logician or just to gain a ``feel" for this or that system. MaGIC has already been used by the first author in the course of researches reported in \cite{SCon}, \cite{FMOD} and \cite{CADE}, while earlier prototypes of the program were essential to \cite{CDM}, \cite{SDM} and \cite{ACT}.\@ Output from MaGIC is also being used in work on theorem provers for non-classical logics along the lines of \cite{ATP}. \smallskip Searching for matrices of this kind is extremely difficult, since the na\I ve search space for $n\times n$ matrices is of size $n^{n^2}$, meaning that the problem grows explosively as $n$ increases. It follows that sheer hardware performance is insufficient to advance any simple solution very far. With a sophisticated generating algorithm such as that used in MaGIC, however, the situation is different. As the size of the matrices increases the time taken per matrix generated also increases, but much more slowly than even we thought possible before such algorithms were developed. Thus even a linear improvement in processing speed can now yield a noticable advance in generating capacity. The present version of MaGIC was written to run under Unix on almost any machine, and has been parallelised to run on a shared memory multiprocessor such as the Sequent Symmetry on which it was actually developed. The parallel program takes full advantage of the coarse grain parallelism inherent in the application to achieve speeds not otherwise reachable at anything like the price. Moreover, the parallelism will easily scale up to make use of many more processors should they be available on larger machines now or in the future. In parallelising the algorithm we made heavy use of the Portable Monitor Macro Package developed at the Argonne National Laboratories by members of the Advanced Computer Research Facility. This allowed quick production of portable and reliable high level code. \smallskip Two programs are shipped in the package. The first is simply called `magic' and runs the matrix generator with a teletype interface which works on just about any terminal. It may be invoked with a switch `$-$x' which suppresses system calls and simplifies certain passages of dialogue in order to make it easy to interface MaGIC via pipes or over a network. The second program shipped is `xmagic' which is an X Windows front end managing the interface with `magic' while providing the advantages of a modern window-based environment for the user. Our preferred setup is to run the X Windows front end locally on a workstation and have it talk through a pipe to MaGIC itself which is running remotely on a more powerful machine, perhaps using many processors in parallel. This arrangement is very easily varied however: see the Installation Guide below. \smallskip One decision which had to be made early in the piece was whether to maximise flexibility or power. MaGIC really works on just one connective, the implication ``$\CC$". The matrices for other connectives are either read in from an input file or defined in terms of the given ones. This means that quite a large amount of logic is assumed (see \S4 for an account of how much) so the range of systems for which MaGIC is suitable is somewhat restricted---only somewhat, be it noted, since the assumed logic is the relatively stable base invariant over many interesting logics. The pay-off for this restriction in range is a great gain in efficiency, since features of the target logics can be used to prime the search space. The problem of matrix generation is, as noted above, subject to a violent combinatorial explosion which starts rumbling when the matrices get to size 4$\times$4 and which defeats most algorithms at size 5$\times$5. Space priming using logical properties is thus necessary to all known methods of generating larger models. An outline of the technique will be found in \S5. In MaGIC we have tried to strike a balance between efficiency and range; if we have erred it is on the side of efficiency, since a program that does a hundred things, or even ten things, and does them well is better than one that offers a million varieties of nothing. We are acutely aware that a program of this type {\em could\/} be generalised to produce algebraic structures meeting arbitrary specifications, but we feel that application-specific adaptations got by changing the IO and testing routines while leaving the core of the program untouched would typically out-perform a general-purpose generator. \smallskip \S2 of this exposition is the Installation Guide for MaGIC 1.1\@. In \S3 are some tutorials which we recommend as an introduction to using the program together with definitions and descriptions of the various menu options. \S4 contains a brief discussion of the use of matrices to model propositional logics and of the kind of model for which MaGIC searches. It also details the logics and fragments of logics available. \S5 is an overview of the algorithm instantiated by MaGIC. It is intended to be explanatory, and useful to anyone proposing to customise or adapt the program to their own purposes or to write their own model-generators using other techniques in place of ours. Finally we give some records of MaGIC's performance indicating the degree of parallelisation achieved and the effects of various ways of using the program's features. \smallskip The following is a summary of the main differences between versions 1.0 and 1.1 of MaGIC and of xmagic. \begin{itemize} \item MaGIC 1.1P has as an additional feature dynamic selection of the number of processes via menu option `\#'\@. Unlike MaGIC 1.0P it does not hang if processes fail to be forked but extricates itself gracefully. \item MaGIC 1.1 has more efficient definitions of the pre-defined logics than MaGIC 1.0, so it runs over 25\% faster on certain jobs. \item The runtime statistics given by MaGIC 1.1 include cpu time as well as elapsed time if the header \verb|times.h| is available. \item Xmagic 1.1 now does more checking that its settings accord with those of the MaGIC it is running. One outcome is that it displays formulas as parsed by MaGIC rather than simply as typed by the user. \item Xmagic 1.1 uses release 4 of Athena Widgets instead of release 3\@. One difference this makes is to the speed of the text widgets. Another is that RETURN suffices to send selections---this is an alternative to using the \framebox{change} buttons. Another welcome difference is that there is now no problem in popping down the popup sub-widgets. \item There have been numerous cosmetic changes to xmagic. Most obvious is that it has default colours instead of a monochrome display. \end{itemize} Several bugs in 1.0 have been fixed for 1.1\@. The most important are as follows. \begin{itemize} \item In MaGIC 1.0 the action on satisfaction of user-defined axioms was incorrect so that certain good matrices failed to be found. This is corrected in 1.1. \item On certain very large jobs TRANSREF was (rarely) repeating itself so that some matrices were found twice. This was a small bug but potentially serious as TR.c has applications beyond MaGIC. \item MaGIC 1.1, unlike 1.0, stops on time even if no matrices are found. \item MaGIC 1.1 does much better garbage collection in the routine for eliminating isomorphisms than did 1.0\@. This speeds up execution a little and avoids some mysterious crashes. \end{itemize} \smallskip In our experience, everyone who takes an interest in a program of this type which does something useful soon wants to know why it doesn't do something else. MaGIC is so written that it is fairly easy to adapt it to search for models of different systems, having different connectives for instance. Changing the stock of user-defined axioms quite simple though not quite trivially so. Adding a new pre-defined logic is rather more complicated but still not a major change. Altering the list of pre-defined connectives is yet more intricate but still feasible. As we urge again in \S3 below, please contact us if you want to customise MaGIC in any of these ways. We will either change it for you (which may take a while) or, if you are an experienced C programmer, advise you on how to do it yourself. As we also note below, alterations in MaGIC tend to require matching alterations to xmagic. Hence doing it yourself could create incompatibilities between MaGIC and xmagic. While we have no wish to discourage you from experimenting with similar code or from amending the program to suit your purposes---it is a research tool, after all, not a display piece---we do recommend that you enlist our co-operation if only in the interests of sanity. Our address is: \bigskip\begin{center} Automated Reasoning Project \\ Australian National University \\ GPO Box 4, \ Canberra, \ A.C.T. 2601 \\ Australia \\[2mm] gustav@arp.anu.oz.au, \ or \\ jks@arp.anu.oz.au \end{center} .