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