
\newpage
\begin{center}
{\Large\bf III}

\vspace{3mm}
{\large\bf USER'S GUIDE TO MaGIC}
\end{center}

\vspace{12mm}\noindent
{\large\bf \S3.1\hs{3mm}A MaGIC Tutorial}

\bigskip
This section assumes that you have access to the program MaGIC 
which generates matrices suitable for modelling a wide selection 
of logics.  First we shall step through some uses of MaGIC in 
its simplest form, with just a ``dumb terminal" display and 
keyboard input.  It is suggested that you start here even if you 
intend to run the program from X Windows, since the xmagic 
tutorial given later will assume you already have some idea 
of what MaGIC itself is doing.  The installation of MaGIC should 
have placed the executable file `magic' in your ordinary path.  If 
this has not been done, you may have to change directory or change 
your path specification so as to make the binary accessible.  Then type
\begin{quote}
prompt\% \ {\bf magic}
\end{quote}
You should now have a display like this:
\begin{verbatim}

   This is MaGIC, finding matrices for your favourite logic.
   Matrices come in all sizes up to 16x16.


   What is your favourite logic?  
 
\end{verbatim}
Our first aim is to inspect the {\bf R} matrices of sizes up 
to 4$\times$4, so type in {\bf R} and hit {\fns\bf RETURN}.  
The display changes to 
\begin{verbatim}

   Logic:        R

   Fragment:     ->, &, v, ~, o, t, f, T, F

   TTY output:   pretty
   File output:  none

   Search concludes when size 14 finished.


      A)xiom    B)adguy    C)onnective   D)elete
      E)xit     F)ragment  G)enerate     H)elp
      I)O       J)ump      K)ill         L)ogic 
         
\end{verbatim}
This is in two parts.  First comes a report on the job we are 
currently asking MaGIC to do, and second comes a menu of options 
mostly for making changes to the job.  If you like, type {\bf h} 
now to see the Help page which briefly describes each menu 
option.  Hitting {\fns\bf RETURN} again gets back the display.

\smallskip
You will see from the display that we want matrices for the logic 
{\bf R}, that we want all the standard connectives to be defined, 
that we want pretty (human-readable) printing of the matrices to 
the screen, that we have not requested any file output and 
finally that MaGIC is to generate all the {\bf R} matrices up to 
14$\times$14 (the end of its input file).  This last we do {\em not} 
want, so we should set a more appropriate ``jump" condition.  Type 
{\bf j} and {\fns\bf RETURN} to do this.  MaGIC asks
\begin{verbatim}
   Shall I stop when: (a) I'm exhausted?
                      (b) time's up?
                      (c) I've found enough matrices?
                      (d) the matrices get too big?
                      (e) a combination of the above?
\end{verbatim}
and the answer is {\bf d}, so type it (and {\fns\bf RETURN}).  4 
is big enough, so reply {\bf 4}.  When the display comes back the 
`14' will have changed to a `4'.  We are now ready to go, so take 
menu option {\bf g} and don't blink.

\smallskip
I hope you memorised those six matrices.  To look at them at more 
leisure we can send them to a file.  Continue and take option 
{\bf i} from the menu.  MaGIC now asks what sort of printout we 
want on our screen (the answer is {\bf p} for ``pretty") and then 
what sort of printout we want filed.  Answer {\bf p} again, after 
trying {\bf h} if you like.  We are now asked to name an output 
file, so name one.  Now the display has changed to record that we 
have asked for pretty output to be sent to the named file.  Type 
{\bf g} again to get the matrices.  Notice the runtime statistics 
printed at the end of the job.  The program found the 6 good 
matrices (i.e.\ ones satisfying all the {\bf R} postulates) 
without wasting time testing a single bad one---well, it does 
work by MaGIC.

\smallskip
This time, after typing {\fns\bf RETURN} to continue, take menu 
option {\bf e} to exit from MaGIC.  Either throw your file of 
matrices up on the screen using {\bf more} or {\bf less}, or 
print them out on your friendly neighbourhood line printer.  Get 
to look at them, anyhow.

\smallskip
Your file first contains a copy of the display to record what it 
is we are looking at.  Then the matrices are ordered by size 
(number of values), secondarily by choice of negation table, 
under that by choice of lattice order (for conjunction and 
disjunction) and finally by implication table.  The first matrix 
in the file, the only one of size 2, is the classical truth table 
structure.  I take it this is too familiar to be worth perusing 
much at this point, so let us inspect the one and only 3-element 
matrix which follows it:
\begin{verbatim}
Size: 3

    Negation table #1   ~ | 0 1 2
                        --+------
                          | 2 1 0


    Order #1     < | 0 1 2
                 --+------
                 0 | + + +
                 1 | - + +
                 2 | - - +

    Choice of t: 1

    Matrix # 1       -> | 0 1 2
                     ---+------
                      0 | 2 2 2
                      1 | 0 1 2
                      2 | 0 0 2
\end{verbatim}
The negation table tells us that while the top and bottom 
elements (2 and 0 in this case) are as always the negations of 
each other, there is in between an element (1) which is a fixed 
point for negation: for this element $a=\,\N a$.  Well, it is 
reasonably well known that {\bf R} tolerates such things.  Now 
the order table, as might be expected, tells us that we have a 
total order or chain, with 0 at the bottom, 1 in the middle and 2 
at the top.  The constant t, the least of the designated values, 
is 1, so 2 is also designated (true) as the order table has \ + \ 
for \ (1,2)\@.  It is interesting that the ``paradoxical" value 1 
which is its own negation is {\em true} according to this 
structure.  Whatever we may make philosophically of this, the 
$\CC$ matrix definable on it does make all the axioms of {\bf R} 
come out with designated values for all assignments, and the 
truth on such assignments is closed under the rules of inference.
Hence it is an {\bf R} matrix within the Meaning of the Act.  In 
fact, it is quite a famous one noticed by Soboci\'nski as long 
ago as 1952 and appearing in \cite{ENT}, on pages 98 and 148.

\smallskip
We shall now try to make MaGIC work a bit harder.  Start up the 
program again by typing {\bf magic} and again ask for logic 
{\bf R}.  This time we shall look for matrices to refute some bad 
guys (defined for this purpose as non-theorems of {\bf R}).  In 
each case we want MaGIC to jump out of the search when it finds 
one refuting matrix, so take menu option {\bf j} and this time 
reply to its question with {\bf c} followed by {\bf 1}.  If you 
now type {\bf g} you will get ``truth tables", the first {\bf R} 
matrix to be found.  Using the full might of MaGIC to generate 
this is a bit like commuting to work in a Space Shuttle, but 
never mind.  Take option {\bf b} in order to define a formula 
which is to {\em fail\/} in any ``good" matrix.  In reply to 
\begin{verbatim}
   Enter formula (or RETURN):
\end{verbatim}
type the well-known classical theorem
$$ \mbox{{\bf p $-\!\!>$ (q $-\!\!>$ p)}} $$
using \ \verb|minus| \ followed by \ \verb|greater than| \ to 
make the arrows.  This time on taking option {\bf g} we get the 
three-element matrix again (its standard name according to 
\cite{CDM} is {\bf R3.1a1.1}, by the way) only this time the 
program has added the legend
\begin{verbatim}
   p = 1  q = 2
\end{verbatim}
This is the assignment of values which falsifies our bad guy.  If 
$p$ is assigned 1 and $q$ is assigned 2 then $q\C p$ gets to be 
$2\C 1$ which is 0, so the bad formula is $1\C 0$ which is 
likewise 0.  The runtime statistics this time record that a 
``bad" matrix was tested.  This was the two-element truth table 
one which, though it satisfies all the postulates of {\bf R}, is 
bad because it does not refute the formula we wanted to fail.
If you are running a parallel version of MaGIC you may have noticed 
that the program took several seconds over finding the matrix.  This 
was because we did not set an upper bound on the size of matrices in 
which MaGIC was to look so it read in and prepared for searching 
{\em all\/} the setups for {\bf R} matrices up to size 14.  Try setting 
a more sensible jump condition by taking {\bf j} and choosing jump option 
{\bf e}.  One matrix is enough; it can get, let us say as big as size 6; 
we do not wish to set a time limit, so we answer 0 to `how many seconds". 
This time on taking option {\bf g} we should get a more speedy answer.

\smallskip
Now let's try another formula:
$$ (p\K\N p)\C(q\A\N q) $$
This one is valid in all the matrices we have seen so far, but is 
not a theorem of {\bf R}. Take menu option {\bf b} again and type 
it in as before.  This time on taking option {\bf g} we find we 
have to wait a few seconds for MaGIC to sort through some rather 
larger matrices.  What it comes up with eventually is a 
6$\times$6 specimen, {\bf R6.2b1.1} in the jargon of \cite{CDM}.  

\smallskip
{\bf R} matrices of that size are not really stretching MaGIC, 
however, so now we'll set it a real problem.  The first move is 
to define a new connective (really just an abbreviation).  Take 
menu option {\bf c}.  We are asked to
\begin{verbatim}
   Type the new connective:
\end{verbatim}
and we type an asterisk \ {\bf *}\@.  Its adicity is 1, so when 
MaGIC asks, type {\bf 1}.  Now we define \ *a \ by typing \ 
{\bf a $-\!\!>$ t}.  When the display returns, notice that the 
newly defined connective is listed.  Take menu option {\bf b} 
again and this time type
$$ \mbox{{\bf **(f \& t) v (f \& t $-\!\!>$ *f)}} $$
Set a combination jump condition again (option {\bf j} followed by 
{\bf e}), this time allowing the matrices to get up to size 10 as 
well as forcing a halt when one matrix is found.  Take option 
{\bf g} and go out and make yourself a coffee
\ldots\ldots

\smallskip\noindent\ldots\ldots\ 
After a decent interval (about 50 seconds on our workstation) 
MaGIC reports back with a 10$\times$10 matrix, to be found in 
\cite{CDM} under the instantly forgettable name of 
{\bf R10.1a2.2} and in \cite{SDM} as {\bf C6}\@.  What you have 
before you this time is quite non-trivial.  This matrix and its 
significance for the {\bf R} theory of the sentential constants 
t and f were not discovered until 1979 and not published until 
1985.  You may think it took MaGIC a long time to think up just one 
matrix, but consider that it had to traverse the 10$\times$10 search 
space (na\I vely $10^{100}$ possible matrices) to find this single 
needle in a truly enormous haystack.

\smallskip
If you are running the sequential program skip this paragraph. 
To demonstrate the virtues of running MaGIC 1.1P in parallel, we may change 
the number of processors in use.  By default two processes are started when 
the program is loaded: this is the minimum for successful execution of the 
parallel version, as one process looks after IO leaving one to do the 
generating of matrices.  It is assumed that on suitable hardware each 
process is executed by a different processor.  To change the number of 
processes to, say, 5 simply type \ {\bf \#5} \ in place of a menu selection. 
The top line of the display (not present in the sequential version of the 
program) should change to
\begin{verbatim}
     Parallel MaGIC running 5 out of 8 processes
\end{verbatim}
There are now four ``slave" processes to generate matrices instead of one.  
If you now try running the last job again you will be able to measure the 
difference this makes to the speed of execution.  This time we do not 
expect you to get your coffee before the matrix is found.  How does the 
speedup factor compare with the maximum possible which is equal to the 
number of slaves?  

\smallskip
The number of processes can be pre-selected by using the command line 
switch \ {\bf $-\#n$} \ where $n$ is an integer greater than 1 and at most 
equal to the number of processors on your machine.  To start up with 5 
processes, for example, the command line reads
\begin{quote}
prompt\% \ {\bf xmagic $-\#5$}
\end{quote}
If for some reason such as lack of swap space one or more processes fail to 
be created MaGIC will inform you of this and set itself up with the maximum 
number of processes actually available.

\smallskip
You have now had some experience of getting MaGIC to perform its 
tricks, at least on one of the logics it knows about.  For 
information on the other logics see \S4 below.  For more detail 
of the menu options, read on.  Meanwhile, you have learned to use 
a power tool; may it bring you many happy implications.

\newpage\noindent
{\large\bf \S3.2\hs{3mm}The Menu Options}

\bigskip
This section contains definitions and descriptions of the various 
commands accepted by the program MaGIC.  Details of the logics 
and fragments with which it deals will be found in \S4 below.  
For details of how to install the program see the Installation 
Guide in section \S2 above.  For an account of the X Windows 
interface see the next section.

\hugeskip\noindent
{\bf a: Adding axioms}

\smallskip
In order to extend the range of logics available through MaGIC 
extra axioms may be added by means of menu option {\bf a}.  The 
additional axioms are of two sorts: pre-defined and user-defined. 
The pre-defined axioms are displayed when option {\bf a} is 
selected; to add one of them simply type its number. User-defined 
axioms are formul\ae\ you type in yourself and may involve 
user-defined connectives as well as the standard ones.  To define 
an axiom you take option {\bf a} and select the number listed as 
``user-defined axiom" (\#19 in most versions of MaGIC)\@.  
Pre-defined axioms are implemented very efficiently by the 
program, whereas user-defined ones are simply evaluated for all 
assignments of values after each matrix passes the pre-defined 
tests. Heavy reliance on user-defined axioms slows down execution 
markedly.  It follows that you should get as close as possible to 
your target logic with the pre-defined logics and axioms before 
throwing in any user-defined ones.  See {\bf b} for information 
on typing formul\ae.

\smallskip
The list of pre-defined axioms supplied with MaGIC is
\begin{verbatim}
   1    p v ~p
   2    (p & ~p) -> q
   3    (p & ~p) -> (q v ~q)
   4    (p & (p -> q)) -> q
   5    p -> (q -> p)
   6    p -> (q -> q)
   7    p -> (p -> p)
   8    (p -> ~p) -> ~p
   9    (t -> p) -> p    equivalently    ((p -> p) -> q) -> q
   10   p -> (t -> p)
   11   p v (p -> q)
   12   T -> (F -> F)
   13   (q -> p) -> ((p -> q) -> (p -> r))
   14   (p -> q) -> ((q -> r) -> (p -> r))
   15   p -> ((p -> q) -> q)
   16   (p -> (p -> q)) -> (p -> q)
   17   (p -> (q -> r)) -> (q -> (p -> r))
   18   ((p -> q) & (q -> r)) -> (p -> r)
\end{verbatim}
This list may be changed, but only the authors really know how.  If you 
want to customise MaGIC in this way, contact us directly.

\smallskip
Note that adding an axiom which is already valid in your selected logic 
(e.g.\ adding axiom 15 to the logic {\bf R}) has no effect on the 
generation of matrices.  Such redundant axioms are automatically 
de-selected by MaGIC during the matrix search, in which case they will 
have disappeared from the display when this returns.

\hugeskip\noindent
{\bf b: Defining a Bad Guy.}

\smallskip
Menu option {\bf b} allows you to define a formula which must be 
{\em invalid\/} in a matrix for that matrix to count as ``good".  
Each matrix printed in ``pretty" format (see {\bf i}) is 
annotated with an assignment of values to the variables which 
gives the bad guy an undesignated value.  There are no 
pre-defined bad guys: you have to define them yourself.

\smallskip
MaGIC makes use of the following conventions on the typing of formulas.  
Parentheses go around each subformula with a {\em dyadic\/} main 
connective.  There are several ways of reducing their number.  
Firstly, all monadic connectives such as negation have minimal scope.  
Secondly, extreme outermost parentheses are redundant and will be 
ignored.  Secondly, the dyadic connectives are ranked
$$ \fs\:\:\K\:\:\A\:\:\C $$
followed by any user-defined connectives, in order of increasing scope 
(decreasing ``tightness of binding").  So for example
$$ p\CC q\fs p\K r $$
is parsed as
$$ p\C((q\fs p)\K r) $$
Thirdly, a dot may replace a left parenthesis whose right mate is to be 
imagined immediately before the first following right parenthesis 
unmatched by an intervening left one, or at the end of the formula by 
default.  That is, its mate is as far to the right as is reasonable.  
Finally, unless parentheses or scope conventions dictate otherwsise, all 
association is to the left.  So
$$ (p\Cdot q\C r)\Cdot s\C q\Cdot p\Cdot s\C r $$
is parsed as
$$ (p\C(q\C r))\C((s\C q)\C(p\C(s\C r))) $$
For specifying formul\ae\ only the four variables 
$$ p\:\:q\:\:r\:\:s $$
are available.  It pays to use the ``lowest" variables (i.e.\ $p$ first, 
then $q$) as much as possible since this speeds up the search.  Another 
finesse is to give short axioms before long ones as for technical 
reasons this is statistically likely to speed things up a little.

\hugeskip\noindent
{\bf c: Defining new connectives}

\smallskip
Option {\bf c} of the menu allows you to introduce new 
connectives in order to abbreviate cumbersome expressions or to 
make user-defined axioms and bad guys more readable.  Definitions 
may be nested, one user-defined connective being used in the 
definition of another.  For example, it is often useful to define 
certain modal operators thus:
\begin{verbatim}
   Definitions:  La       t -> a
                 Ma       ~L~a
                 a * b    M(a & b)
\end{verbatim}
Note that all such definitions are purely abbreviatory: MaGIC 1.1
does not support contextual or inductive definitions.

\smallskip
The conventions for typing the formul\ae\ in definitions are 
the same as for axioms and bad guys (see {\bf b} except that 
`a' and `b' are used as variables instead of `p' and `q'.

\smallskip
There is a maximum number of defined connectives.  By default 
(when MaGIC is supplied) this is 5; it can be changed\footnote{It is 
changed by altering the constant \verb|CMAX| in \verb|MaGIC.h| before 
compilation.} but note that any such change will not be recognised by 
the X Windows interface xmagic.

\smallskip
Defined connectives can be of adicity (number of argument places) 
0, 1 or 2.  Any of adicity 0 must be compounded from the sentential 
constants t and f, and the definitions of monadic or dyadic 
connectives must involve the right number of variables.  The formula 
used as definition must consist of more than one character (so it is 
not permissable to rename T as U, for instance, though why you should 
want to is entirely obscure).  It is also impermissable to use the 
formula $p$ on its own either as axiom or as bad guy.  If you are so 
perverse as to want a formula which fails in every matrix, use $q$.

\hugeskip\noindent
{\bf d: Deleting Axioms and Bad Guys}

\smallskip
After selection of menu option {\bf d} you are offered the choice 
of deleting a pre-defined axiom, a user-defined axiom or the bad 
guy.  Attempting to delete where there is nothing to delete has 
no effect.

\smallskip
Deletion cannot be used to {\em subtract\/} axioms from the 
chosen logic.  If you want to do this you must choose a weaker 
logic and add axioms to it.

\smallskip
There is no need to delete the bad guy if you just want to change 
it.  Taking option {\bf b} and typing a formula automatically removes the 
old bad guy.  However, taking {\bf b} and passing MaGIC the null formula 
has no effect, so that is {\em not\/} a way of deleting the bad guy.

\smallskip
User-defined connectives cannot be deleted.  This does not really 
matter much, as you can leave them unused.  However, they can 
affect the chosen fragment by forcing certain connectives to be 
available.  To get rid of them you must kill the job with option 
{\bf k}.

\hugeskip\noindent
{\bf e: Exit}

\smallskip
Menu option {\bf e} clears the screen, closes any files used 
and shuts down MaGIC cleanly, returning to the system.  The 
parallel version of MaGIC also has to wait for all of the ``slave" 
processes to die before it can complete its exit, so in some cases 
you may find you have to wait a few seconds for this to happen.

\hugeskip\noindent
{\bf f: Choice of Language Fragment}

\smallskip
MaGIC offers quite a wide choice of pre-defined connectives.  
Implication is of course compulsory, but everything else is 
optional.  The most common choices of fragment are
\begin{enumerate}
\item Pure implication.  Just the connective $\CC$.
\item Implication and negation.  $\CC$ and $\N\;$.
\item Positive logic.  $\CC$, $\&$, $\A$, t, T.
\item Full logic.  $\CC$, $\N\,$, $\,\&$, $\A$, $\,\fs$, t, f, T, F.
\end{enumerate}
The full logic is the default.  Fusion $\fs$ may optionally 
be added to any fragment of any logic, though in the case of 
the very weak non-affixing system {\bf FD} it is discouraged 
because MaGIC's efficient strategy for incorporating it 
depends on affixing.

\smallskip
Because of inbuilt or axiomatic relationships between the 
connectives certain fragments bring extra connectives along.  For 
example, if \& and $\A$ are defined so are t, T and F, while if 
$\N$ \ is defined \& brings along f as well.  The false constant 
f is by definition $\N\;$t, so it is available if and only if 
negation and t are in the fragment.  For a fuller account of the 
fragments and dependencies see \S4.2 below.

\smallskip
The maximum matrix size is different for certain different 
fragments.  For the full logic it is 14 with distribution, 10 
without distribution and 16 with total order; for positive logic 
it is 10 with distribution, 8 without and 12 with total order; 
for implication-negation it is 8 with t and 7 without; for pure 
implication it is 6 and for implication with t it is 7.  If your 
selected postulates include enough to force the structures to be 
boolean algebras the 16-element one is offered as well as the 8.

\smallskip
If a user-defined connective or axiom appeals to a connective not 
in the currently selected fragment, the fragment is automatically 
enlarged to include it.  For this reason it may be impossible to 
make the fragment smaller without killing the job in order to 
eliminate some definition.

\hugeskip\noindent
{\bf g: Generating Matrices}

\smallskip
Menu option {\bf g} runs MaGIC on the chosen job.  The sizes, 
negation tables (if negation is defined), partial order tables 
and choices of designated values are read from an input file and 
the program searches for possible implication matrices within 
those constraints.  ``Good" matrices, satisfying all the chosen 
conditions, are printed in the chosen formats (see {\bf i}) to 
the user's video screen and to the output file if any.  At the 
end of the run, some brief statistics are given, the most 
important for general purposes being the total number of good 
matrices generated and the time taken.

\smallskip
Only one matrix from each isomorphism class is returned.  The 
input files do not contain isomorphic copies of setups, so most 
isomorphisms are eliminated at the input stage.  A few residual 
cases have to be cleaned up by MaGIC itself.  The ``isomorphs 
omitted" line in the runtime statistics records how many.

\hugeskip\noindent
{\bf h: Help}

\smallskip
The {\bf h} menu option simply transfers to the screen a page 
describing in brief what each item on the menu does.  Further 
Help pages are offered at various points: for example, there is 
one on typing formul\ae\ and another giving the axioms of the 
various logics.

\hugeskip\noindent
{\bf i: I/O Selections}

\smallskip
Really just output selections, but I couldn't get `output' to 
begin with an `i'.  Menu option {\bf i} causes MaGIC to prompt 
for the specifications of output formats first for the screen and 
then for the output file.  The formats are:
\begin{description}
\item[pretty] Human-readable output, the default for tty.  
Matrices are printed in squares with row and column labels.  
Hexadecimal notation is used so that all values are single 
digits.  If pretty file output is requested, the job description 
also goes into the file.  A size, negation table, order structure 
or choice of designated values is printed only if there is at 
least one good matrix under it.  The numbering of negations, 
orders and implication matrices is incremental within each job, 
not absolute.  So one and the same partial order, for example, 
might get the label 4.16 when {\bf TW$_{\,\C}$} matrices are 
being generated but 4.5 when {\bf R$_{\,\C}$} matrices are the 
subject.
\item[ugly] Machine-readable output consisting entirely of 
integers.  `$-1$' is used to indicate that there are no more 
tables of a given class (e.g. no more negation tables of the 
current size) to come.  The one concession to human scanning 
is that a line feed is inserted after each matrix.  The 
conventions such as `$-1$' separators are the same as for 
MaGIC's data files.  The exact syntax of ugly files is given below in 
\S3.3.
\item[summary] Only the numbers of matrices are printed. This can 
be used for instance to check the size of a job where the output 
might otherwise be unmanageably large.  It is also used to 
benchmark matrix-generating programs as it eliminates variation 
due to I/O features.
\item[none] No output is produced.  This is the default for file 
output.  There is, of course, little point in choosing this 
``format" for both file and tty!
\end{description}

\smallskip
Every time you take option {\bf i} and nominate non-null file 
output you are asked to name or invited to rename the output 
file.  If the file you name already exists then the matrices are 
appended to the end of it, so it is never over-written.  It is 
saved to disk after each run (i.e. each call of {\bf g}), so if 
you somehow crash at least your previous matrices are safe.

\hugeskip\noindent
{\bf j: Jump Conditions}

\smallskip
Menu option {\bf j} allows you to set the condition on which 
MaGIC jumps out of the search.  The options are:
\begin{description}
\item[End of input.] MaGIC stops when it comes to the end of its 
input file.  That is, it runs as long as possible.  This is the 
default option and overrides any other selection.
\item[Timed out.] Stop after the specified number of seconds.  The 
minimum selectable time is 5 seconds: any attempt to set a time 
less than this will be counted as 0\@.  Note that MaGIC may take a 
little time to close down the search gracefully.  Thus if you ask for 
a 60-second run MaGIC may well run for 61.3 seconds or something of 
that sort. It halts as soon after the end of the specified period as 
there it conveniently can.
\item[Enough found.] Stop as soon as the total of ``good" 
matrices found equals the specified number of matrices.  The 
commonest use of this option is to stop when 1 matrix is found to 
refute a bad guy.
\item[Size limit.] Stop when the number of values threatens to 
exceed the specified maximum.  Since the data files are all 
organised in ascending order of size this means MaGIC should 
generate all matrices of the chosen sort up to and including the 
size you specify.  Attempting to set a size limit bigger than the 
pre-defined maximum (e.g. bigger than 8 in the 
implication-negation fragment) has no effect at all.
\item[Combination] This option allows you to set a time limit 
{\em and\/} a size limit {\em and\/} an upper bound to the number of 
matrices. The conventions for each are as above.  MaGIC stops 
generating as soon as any one of the limits is reached.  Giving 0 as 
one of the limits disables that option.  Thus if you want to generate 
up to 100 matrices in 30 seconds, but do not care how big they get, you 
may take option {\bf e}, specifying the time limit as 30, the maximum 
number of matrices as 100 and the size limit as 0.
\end{description}

\hugeskip\noindent
{\bf k: Kill the present job}

\smallskip
Menu option {\bf k} causes all settings to be re-initialised and 
MaGIC to return to the start of the execution.  Any matrices 
written to an output file are saved therein before this happens.

\hugeskip\noindent
{\bf l: Choice of pre-defined logic}

\smallskip
Before MaGIC will do anything it needs to know which logic the 
matrices are to validate.  The logics it recognises are 
$$\mbox{{\bf FD \ \ B \ \ DW \ \ TW \ \ T \ \ E \ \ R \ \ C \ \ CK \ \ S4}}$$
For axiomatisation and brief description of these see \S4.3.  The 
program has written into it efficient methods of setting up the 
search space appropriate to each of these, so it is best to 
choose the strongest logic that is no stronger than you want and 
add a minimum of axioms to it.

\smallskip
It is not difficult for an experienced C programmer with some 
knowledge of non-classical logic to change the list of logics in 
order to adapt MaGIC to your purposes.  Exactly how this is done, 
however, is too involved for these notes.  If you wish to customise 
MaGIC in this way, contact the authors.

\hugeskip\noindent
{\bf \#: Number of processes}

\smallskip
To change the number of processes with which the parallel version of 
MaGIC operates type a hash (\#) followed immediately by the desired 
number.  This must be an unsigned integer greater than 1 (since the 
minimum configuration is a master process to look after IO and a slave 
to do the searching) and no greater than the number of processors on 
your hardware.  It is assumed that each process will be executed by 
one processor, though in fact the process-creation macro simply uses 
the Unix \verb|fork()| function, so nothing prevents one processor 
running several processes pseudo-concurrently by swapping.  Demanding 
an illegal number of processes has no effect beyond eliciting an error 
message.  To the sequential version of MaGIC the menu option {\bf \#} 
makes sense but has no effect whatever.  The same hash notation for 
number of processes can be used (with a leading `$-$') as a command 
line option.

\newpage\noindent
{\large\bf \S3.3\hs{3mm}The Ugly Data Format}

\bigskip
Somewhere on your system is MaGIC's data directory which contains some 
short files of text to be sent to the screen---for example giving certain 
information in response to requests for help---and several longer files of 
integers which represent the data structures to be read in by the program 
in order to avoid having to re-calculate the setups within which to search 
for matrices.  The syntax of the input files for cases in which negation is 
undefined may be specified by means of a flow diagram thus:
$$\begin{picture}(0,12)(0,-6)
\put(-6,2){\framebox(2,2){siz}}
\put(-1,2){\framebox(2,2){$\leq$}}
\put(4,2){\framebox(2,2){des}}
\put(-6,-4){\framebox(2,2){`-1'}}
\put(-6,-1){\framebox(2,2){`-1'}}
\put(-1,-1){\framebox(2,2){`-1'}}
\put(-8,3){\vector(1,0){2}}     % into siz
\put(-4,3){\vector(1,0){3}}     % siz to ord
\put(1,3){\vector(1,0){3}}      % ord to des
\put(6,3){\line(1,0){2}} 
\put(8,3){\line(0,1){2}} 
\put(8,5){\line(-1,0){3}}
\put(5,5){\vector(0,-1){1}}     % des to des
\put(5,2){\line(0,-1){2}} 
\put(5,0){\vector(-1,0){4}}     % des to -1a
\put(0,1){\vector(0,1){1}}      % -1a to ord
\put(-1,0){\vector(-1,0){3}}    % -1a to -1b
\put(-5,1){\vector(0,1){1}}     % -1b to siz
\put(-5,-1){\vector(0,-1){1}}   % -1b to -1c
\put(-6,-3){\vector(-1,0){2}}   % out from -1c
\end{picture}$$
Where negation is defined the syntax becomes:
$$\begin{picture}(0,12)(0,-6)
\put(-8.5,2){\framebox(2,2){siz}}
\put(1.5,2){\framebox(2,2){$\leq$}}
\put(6.5,2){\framebox(2,2){des}}
\put(-8.5,-4){\framebox(2,2){`-1'}}
\put(-8.5,-1){\framebox(2,2){`-1'}}
\put(1.5,-1){\framebox(2,2){`-1'}}
\put(-3.5,2){\framebox(2,2){$\sim$}}
\put(-3.5,-1){\framebox(2,2){`-1'}}
\put(-10.5,3){\vector(1,0){2}}    % into siz
\put(-6.5,3){\vector(1,0){3}}     % siz to neg
\put(3.5,3){\vector(1,0){3}}      % ord to des
\put(8.5,3){\line(1,0){2}} 
\put(10.5,3){\line(0,1){2}} 
\put(10.5,5){\line(-1,0){3}}
\put(7.5,5){\vector(0,-1){1}}     % des to des
\put(7.5,2){\line(0,-1){2}} 
\put(7.5,0){\vector(-1,0){4}}     % des to -1a
\put(2.5,1){\vector(0,1){1}}      % -1a to ord
\put(1.5,0){\vector(-1,0){3}}     % -1a to -1d
\put(-7.5,1){\vector(0,1){1}}     % -1b to siz
\put(-7.5,-1){\vector(0,-1){1}}   % -1b to -1c
\put(-8.5,-3){\vector(-1,0){2}}   % out from -1c
\put(-1.5,3){\vector(1,0){3}}     % neg to ord
\put(-3.5,0){\vector(-1,0){3}}    % -1d to -1b
\put(-2.5,1){\vector(0,1){1}}     % -1d to neg
\end{picture}$$
Here {\em siz\/} is an integer specifying the greatest available value.  The 
partial order of implication symbolised $\,\leq\,$ is written as an array of 
ones and zeros in ascending, row-major order.  The least designated (true) 
value is given as the integer {\em des}.  There are no negative 
values, so the expression `-1' is used to signify that there are no more 
entries in a class.  Negation, where it is defined is specified by 
means of an integer vector.

\smallskip
By way of illustration, here is a truncated data file containing the 
information needed to generate the {\bf R} matrices up to size 4 as in the 
first tutorial.
\begin{verbatim}
     1
     1 0
     1 1 0 1
     1
     -1 -1 -1
     2
     2 1 0
     1 1 1 0 1 1 0 0 1
     1
     2
     -1 -1 -1
     3
     3 2 1 0
     1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1
     1
     3
     -1
     1 1 1 1 0 1 1 1 0 0 1 1 0 0 0 1
     1
     2
     3
     -1 -1
     3 1 2 0
     1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1
     1
     3
     -1 -1 -1 -1
\end{verbatim}
Each line corresponds to one box in the flow diagram, except that successive 
`-1's are collected to save spcae.

\setlength{\unitlength}{5mm}

\smallskip
The syntax of ugly output is exactly the same with the addition of one more 
layer consisting of implication matrices.  These, naturally, are arrays of 
integers given in row-major order.  Thus the flow diagram for the syntax of 
ugly output files reads:
$$\begin{picture}(0,12)(0,-6)
\put(-11,2){\framebox(2,2){siz}}
\put(-1,2){\framebox(2,2){$\leq$}}
\put(4,2){\framebox(2,2){des}}
\put(9,2){\framebox(2,2){$\C$}}
\put(-11,-4){\framebox(2,2){`-1'}}
\put(-11,-1){\framebox(2,2){`-1'}}
\put(-1,-1){\framebox(2,2){`-1'}}
\put(-6,2){\framebox(2,2){$\sim$}}
\put(-6,-1){\framebox(2,2){`-1'}}
\put(4,-1){\framebox(2,2){`-1'}}
\put(-13,3){\vector(1,0){2}}    % into siz
\put(-9,3){\vector(1,0){3}}     % siz to neg
\put(1,3){\vector(1,0){3}}      % ord to des
\put(6,3){\vector(1,0){3}}      % des to aro
\put(11,3){\line(1,0){2}} 
\put(13,3){\line(0,1){2}} 
\put(13,5){\line(-1,0){3}}
\put(10,5){\vector(0,-1){1}}     % aro to aro
\put(10,2){\line(0,-1){2}} 
\put(10,0){\vector(-1,0){4}}     % aro to -1e
\put(5,1){\vector(0,1){1}}      % -1e to des
\put(4,0){\vector(-1,0){3}}     % -1e to -1a
\put(0,1){\vector(0,1){1}}      % -1a to ord
\put(-1,0){\vector(-1,0){3}}     % -1a to -1d
\put(-10,1){\vector(0,1){1}}     % -1b to siz
\put(-10,-1){\vector(0,-1){1}}   % -1b to -1c
\put(-11,-3){\vector(-1,0){2}}   % out from -1c
\put(-4,3){\vector(1,0){3}}     % neg to ord
\put(-6,0){\vector(-1,0){3}}    % -1d to -1b
\put(-5,1){\vector(0,1){1}}     % -1d to neg
\end{picture}$$
We are currently working on utilities to read ugly output files and perform 
arbitrary operations on the algebras encoded therein.  Such utilities will 
be shipped with the next release of MaGIC, though they are not available 
with release 1.1.

\newpage\noindent
{\large\bf \S3.4\hs{3mm}An Xmagic Tutorial}

\bigskip
We now assume you are in a position to run MaGIC in an X Windows 
environment and that the program xmagic has been installed on your 
system.  The simple command line
\begin{quote}
prompt\% \ {\bf xmagic}
\end{quote}
may be enough to run the program, or you may need to specify more 
things---for instance that it is to run on some remote machine and that 
the display is to be sent to your local screen.  At any rate, on the 
assumption that you have started the program and clicked with your mouse 
in the usual way to position the window on the screen you should have a 
display like that in figure 1.
\begin{figure}
\vspace*{9cm}
\special{ psfile=/usr/local/src/magic/doc/xmagic.ps
  hscale=0.75
  vscale=0.75 }
\caption{Main control panel and display window of xmagic}
\end{figure}
This is rather intricate, but not difficult.  Selected values for many 
of the parameters are highlighted.  You will see, for example, that the 
default logic is the weakest implicational system {\bf FD} and that all 
the standard connectives are marked as available.  The first aim, as in 
the plain MaGIC tutorial above, is to generate the {\bf R} matrices up to 
size 4\@.  We must therefore select logic {\bf R} instead of the default 
{\bf FD}\@.  Do this by moving the cursor until it is positioned over the 
\fbox{R} in the \underline{logic} box (top left) and clicking the left 
mouse button.  The \fbox{R} should now be highlighted.  Now we must tell 
MaGIC when to stop by setting the maximum matrix size to 4\@.  Move the 
cursor over to the \underline{maximum size of matrices} box on the right 
and turn it on by clicking on the button marked \fbox{on}\thinspace.  Now 
it should be possible to type text in the box just above that button 
provided the cursor is there.  Make sure it {\em is\/} there and type 
`4'\@.  Now in order to send to MaGIC the message that there is a new 
maximum size you must click on the \fbox{change} button.  Alternatively, 
hitting {\fns\bf RETURN} after typing the `4' has the same effect.  One of 
the commonest slips made with xmagic is to forget to cement a change in 
this way.  Having hit \fbox{change} or {\fns\bf RETURN} you will see, if you 
look closely, that the cursor has moved back to the left side of the box.  
You have now set up the right problem.  It remains to select the desired 
kind of output.  In order to produce the matrices before your very eyes, you 
must click on \fbox{pretty} in the \underline{tty output} box.  No file 
output is wanted yet, so leave the box next door alone.  Click on the 
\fbox{run} button and wait.

\smallskip
The first surprise, given that you did the earlier plain MaGIC tutorial, 
is that the output is so slow.  This is not because MaGIC is running any 
slower but because the kind of text window used for output is slow.  The 
runtime statistics will show that MaGIC actually completed the search, 
including sending the matrices down the output channel, in a fraction of 
a second; the rest of the time was just what it took to get the text from 
xmagic to the screen.  Now if we want to inspect the six matrices without 
the need to file them we can scroll back over them by using the mouse 
with the cursor in the scrollbar on the left in the standard way.

\smallskip
We shall now change the job specification in three ways: by choosing a 
smaller fragment of the logic, by adding axioms to it and by specifying 
a bad guy.  Move the cursor to the \underline{fragment} box and click on 
\fbox{$\!\N\,$} and then on \fbox{$\circ$}\thinspace\@.  The highlights 
should disappear, showing that these connectives are no longer in the 
selected fragment.  The \fbox{f} disappears as well, because in the absence 
of negation it is not defined.  If you were to click on \fbox{$\circ$} 
before \fbox{$\!\N\,$} you would not succeed in removing fusion from the 
fragment because in {\bf R} it is definable in terms of negation and 
implication.  Now we are asking for matrices to validate the positive 
fragment of {\bf R}, and to strengthen the logic somewhat we shall add 
the ``mingle" axiom
$$ p\Cdot p\C p $$
Click on the \fbox{add axioms} button.  A new window pops up in the usual 
X Windows fashion: you must position the cursor and left-click where you 
want its top-left corner to be.  You can move it around by dragging with 
its top bar if you wish.  This window displays the pre-defined additional 
axioms.  Try clicking on a few to select them and clicking again to 
de-select them.  The one we want is \#7, so finally click so as to leave 
just this one highlighted.  Leave the axiom box on the screen for now, and 
move over to the \underline{fail on formula} box to define the badguy.  Turn 
it \fbox{on} by so clicking.  Now with the cursor inside the box you can 
type the formula which is to fail.  Type 
\begin{verbatim}
     p v (p -> q)
\end{verbatim}
and remember to click on the \fbox{change} button to tell MaGIC you have 
finished.  Now click on \fbox{run} to see all the 4-element {\bf RM+} 
matrices.

\smallskip
The feature you really want to use (and have probably played with already, 
despite what you were told as a child) is the scrollbar which controls the 
number of processes.  Alright---go ahead: slide it up and down using any 
mouse button.  As long as you hold down the button you can slide the 
pointer to the desired position.  When you release it the new setting is 
sent to MaGIC.  If you are running the sequential program you can see this 
toy but can't make it go.  In such a case, you are clearly in need of a 
multiprocessor machine.  Apply for one forthwith.

\smallskip
While the program is generating lots of matrices and 
printing them in pretty format, the printing dominates the time taken so 
that there are no great advantages in using many parallel processes.  For 
problems like that earlier suggested, refuting a complicated sentential 
constant in a 10-element structure, however, it should be possible to 
secure a near-linear speedup as long as the number of processes is not too 
large.  Please experiment with this for yourself.

\smallskip
It remains to \fbox{quit} by hitting the button so marked.  Always leave 
xmagic this way if possible, rather than by killing the window, because 
it is running MaGIC somewhere and needs to close that down properly.  If 
this is not done MaGIC may well still be running on a remote host, 
causing you to become unpopular with the other users who may see it as 
less than magical to have their swap space full of useless processes. 

\newpage\noindent
{\large\bf \S3.5\hs{3mm}Xmagic Reference Guide}

\bigskip
This section contains a brief account of the various options available 
from the xmagic control panel.  It should be used in conjunction with 
the reference guide to MaGIC (\S3.2 above).  One or two general points 
are worth making at the outset.  Firstly, to ``click on" a part of the 
display you use the left mouse button if your mouse has more than one.  
Secondly, xmagic follows standard conventions on popping up new windows: 
the  window appears in outline as soon as it is ready.  Move it to the 
desired position with the cursor and click to bring up the full display.  
Thirdly, windows in which you type text are also fairly standard.  The caret 
can be moved by clicking in the window.  To delete a block of text drag the 
cursor across it while holding down the (left) mouse button and then type 
CTRL-w.  Finally, several of the tools have an ``on--off--change" format.  
To set any of these options first turn it \fbox{on}\thinspace, then type in 
your (new) formula, number or whatever, then click \fbox{change} to send 
what you have typed to the program.  Typing {\fns\bf RETURN} is equivalent.  

\hugeskip\noindent
{\bf add axioms}

\smallskip
Click on \fbox{add axioms} to cause the \underline{xmagic: add axioms} 
window to pop up.  Select or deselect axioms by clicking on them.  
Selected ones are highlighted.  MaGIC automatically deselects certain 
redundant axioms when you select \fbox{run}\thinspace\@. See MaGIC {\bf a}.

\smallskip
Click \fbox{define axiom} to cause the \underline{xmagic: define axiom} 
window to pop up.  Type a formula in the \underline{define axiom} box and 
then click on the number you want to give it. It appears with that number 
in the axiom list and may be selected or deselected just like any other 
axiom.  After selection it is reprinted with MaGIC's standard spacing.  
See MaGIC {\bf a} and {\bf d}.

\hugeskip\noindent
{\bf connectives}

\smallskip
Click on \fbox{connectives} to cause the \underline{xmagic: connectives} 
window to pop up.  When this happens the \underline{symbol} box is 
sensitized.  Type a single character in this box and click the 
\fbox{accept} just below it.  By default it is treated as a constant 
(nullary) operator: to give it arity 1 or 2 click as appropriate.  Type 
the definition in the \underline{define connective} box and click on its 
\fbox{accept} to send the definition via the parser to MaGIC\@.  See 
MaGIC {\bf c}.

\hugeskip\noindent
{\bf fail on formula}

\smallskip
To specify a formula to be invalid in all matrices generated click 
\fbox{on} the \underline{fail on formula} box.  Type the badguy in the 
space provided (if it won't fit use defined connectives to shorten it).  
Click \fbox{change} to send the new formula via the parser to MaGIC\@. It 
will be ignored if the parser reports an error.  See MaGIC {\bf b}.

\hugeskip\noindent
{\bf file output}

\smallskip
Default file output is \fbox{none} (highlighted).  Change this if you 
wish by clicking on any other option.  If you do, the \underline{file 
name} box becomes sensitive.  To send file output to a file other than 
xmagic.save just edit the file name.  To cement the change of name you 
must click \fbox{change}\thinspace\@.  See MaGIC {\bf i}.

\hugeskip\noindent
{\bf fragment}

\smallskip
The usual connectives are listed in the \underline{fragment} box.  The 
highlighted ones are selected.  Certain ones force others to be selected 
as described in \S4.2\@.  Clicking on any connective selects or 
deselects it.  See MaGIC {\bf f}.

\hugeskip\noindent
{\bf run}

\smallskip
The \fbox{run} buton is precisely equivalent to MaGIC menu option {\bf g}. 

\hugeskip\noindent
{\bf help}

\smallskip
Click \fbox{help} to cause the \underline{help} window to pop up.  It 
displays its introductory page at this point.  Other pages are listed 
across the top: click to see them.  Use the scroll bar to peruse each 
page.

\hugeskip\noindent
{\bf logic}

\smallskip
Click on the name of any system in the \underline{logic} box to select 
it.  This is equivalent to MaGIC menu option {\bf l} without the T and L 
prefixes to the systems.  See also {\bf order\/} below.

\newpage\noindent
{\bf maximum number of matrices}

\smallskip
Click the \fbox{on} of this box to activate it.  The number can be edited 
at will before you click \fbox{accept}\thinspace\@.  As for MaGIC, giving 
the bound 0 here is equivalent to disabling this option.  See MaGIC 
{\bf j}.

\hugeskip\noindent
{\bf maximum size of matrices}

\smallskip
Click the \fbox{on} of this box to activate it.  The number can be edited 
at will before you click \fbox{accept}\thinspace\@.  If the number you 
specify is greater than the maximum in MaGIC's input file it will stop in 
any case when the file is exhausted.  As for MaGIC, giving the bound 0 
here is equivalent to disabling this option.  See MaGIC {\bf j}.

\hugeskip\noindent
{\bf order}

\smallskip
The type of lattice order to be used for fragments involving \& and $\A$ 
is selected by clicking in the \underline{order} box.  Obviously, for 
fragments not involving these connectives there is no difference between 
choosing lattice order and distributive lattice order.  Choosing total 
order forces the lattice connectives to be part of the fragment.  See 
MaGIC {\bf l}.

\hugeskip\noindent
{\bf number of processes}

\smallskip
The parallel version, MaGIC 1.1P, allows the number of active processes to 
be changed dynamically.  Xmagic provides a scrollbar interface to this 
feature.  Click and hold with any mouse button within the bar to slide the 
indicator up or down.  The currently selected number of processes is shown 
in the square box at the top.  If for any reason the attempt to create a 
new process fails---this can happen particularly if swap space is in short 
supply and you are competing with other users---MaGIC will send a report of 
the matter which xmagic will show in its main text window.  If this happens 
you will just have to run the program with fewer processes than you would 
like.

\hugeskip\noindent
{\bf quit}

\smallskip
Click \fbox{quit} to cause an orderly exit.  You may have to wait a few 
seconds for xmagic to get MaGIC to close down gracefully.  This action 
invokes MaGIC menu option {\bf e}.

\hugeskip\noindent
{\bf reset all}

\smallskip
This takes you back to the defaults for all options. Use it in particular 
when you no longer want certain defined connectives.  See MaGIC option 
{\bf k}.

\hugeskip\noindent
{\bf stop when time exceeds}

\smallskip
Click the \fbox{on} of this box to activate it.  The time can be edited 
at will before you click \fbox{accept}\thinspace\@.  The units may be 
seconds, minutes, hours, days, weeks, fortnights, months or years.  The 
quantities must be unsigned integers.  As for MaGIC, giving a bound of 
less than 5 seconds here is equivalent to disabling this option.  See 
MaGIC {\bf j}.

\hugeskip\noindent
{\bf tty output}

\smallskip
The default is no output to the screen.  Note that this is different from 
MaGIC whose default is `pretty'.  To select any other format just click 
on it.  Note that since the display window of xmagic is an ordinary 
X Windows text widget it supports such operations as scrolling, cutting 
and pasting (including pasting to other windows) and the like.  See also 
MaGIC {\bf i}.

\hugeskip\noindent
{\bf verbosity}

\smallskip
The program may be run in verbose or silent mode.  Silent is the default. 
Click \fbox{verbose} if you wish to see all the text sent by MaGIC to 
xmagic during the course of their dialog.  If you are familiar with the 
menu-driven version of MaGIC this may help you to determine the exact 
semantics of xmagic actions.

.
