\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}