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