Titlepage.tex:\vspace*{10mm}
algebra.tex:the true proposition 1 and the false one 0.  Then the partial 
algebra.tex:$\Leq$ &  0  & 1 \\\hline
algebra.tex:     0 &  +  & + \\
algebra.tex:$\C$ & 0 & 1 \\\hline
algebra.tex:   0 & 1 & 1 \\
algebra.tex:   1 & 0 & 1 \end{tabular}} $$
algebra.tex:What may be unfamiliar is the thought that the `0' and the `1' 
algebra.tex:$$ \begin{picture}(0,4)(0,-2)
algebra.tex:   \put(-5,0){\begin{picture}(0,0)(0,0)
algebra.tex:              \Dt 2,1  \Dt -2,1  \Dt 0,-1  
algebra.tex:              \put(-2.75,0.8){1}  \put(2.5,0.8){2}  
algebra.tex:              \put(0.5,-1.2){0}
algebra.tex:   \put(5,0){\makebox(0,0)
algebra.tex:                    $\Leq$ &  0  &  1  &  2  \\\hline
algebra.tex:                         0 &  +  &  +  &  +  \\
algebra.tex:         $\C_1$ & 0 & 1 & 2 \\\hline
algebra.tex:              0 & 1 & 1 & 1 \\
algebra.tex:              1 & 0 & 1 & 0 \\
algebra.tex:              2 & 0 & 0 & 1
algebra.tex:         $\C_2$ & 0 & 1 & 2 \\\hline
algebra.tex:              0 & 2 & 2 & 2 \\
algebra.tex:              1 & 0 & 1 & 0 \\
algebra.tex:              2 & 0 & 0 & 1
algebra.tex:         $\C_3$ & 0 & 1 & 2 \\\hline
algebra.tex:              0 & 1 & 2 & 1 \\
algebra.tex:              1 & 0 & 2 & 0 \\
algebra.tex:              2 & 0 & 0 & 1
algebra.tex:1. \> 0-adic:  \> t, \ f, \ T, \ F \\
algebra.tex:the {\bf S0.5} of the relevant logics.  {\bf FD} may be presented 
algebra.tex:\begin{enumerate}\setcounter{enumi}{10}
algebra.tex:   \begin{picture}(0,10)(0,-5)
algebra.tex:   \put(0,0){\circle{1.2}}   \put(-3,0){\circle{1.2}}
algebra.tex:   \put(-6,0){\circle{1.2}}  \put(-9,0){\circle{1.2}}  
algebra.tex:   \put(6,-2){\circle{1.2}}  \put(9,0){\circle{1.2}}   
algebra.tex:   \put(-8.4,0){\vector(1,0){1.8}}
algebra.tex:   \put(-5.4,0){\vector(1,0){1.8}}
algebra.tex:   \put(-2.4,0){\vector(1,0){1.8}}
algebra.tex:   \put(0.5,-0.3){\vector(3,-2){2}}
algebra.tex:   \put(0.6,0.2){\vector(2,1){3.3}}
algebra.tex:   \put(3.6,-2){\vector(1,0){1.8}}
algebra.tex:   \put(0,0){\makebox(0,0){{\fns TW}}}
algebra.tex:   \put(-3,0){\makebox(0,0){{\fns DW}}}
algebra.tex:   \put(-6,0){\makebox(0,0){{\fns B}}}
algebra.tex:   \put(-9,0){\makebox(0,0){{\fns FD}}}
algebra.tex:   \put(4.5,2){\makebox(0,0){{\fns C}}}
algebra.tex:   \put(3,-2){\makebox(0,0){{\fns T}}}
algebra.tex:   \put(6,-2){\makebox(0,0){{\fns E}}}
algebra.tex:   \put(9,0){\makebox(0,0){{\fns R}}}
algebra.tex:   \put(9,4){\makebox(0,0){{\fns CK}}}
algebra.tex:   \put(9,-4){\makebox(0,0){{\fns S4}}}
algorithm.tex:$$\begin{picture}(0,10)(0,-5)
algorithm.tex:\put(-2.5,-0.75){\framebox(5,1.5){{\small Search Control}}}
algorithm.tex:\put(-11.5,-0.75){\framebox(5,1.5){{\small Test Matrix}}}
algorithm.tex:\put(6.5,-0.75){\framebox(5,1.5){{\small Front End}}}
algorithm.tex:\put(0,0.75){\line(0,1){1.5}}
algorithm.tex:\put(9,0.75){\line(0,1){1.5}}
algorithm.tex:\put(0,-0.75){\line(0,-1){1.5}}
algorithm.tex:\put(-9,-0.75){\line(0,-1){1.5}}
algorithm.tex:\put(-6.5,0){\line(1,0){4}}
algorithm.tex:\put(6.5,3){\line(-1,0){4}}
algorithm.tex:   #define  FORALL(x)  for (x=0; x<=siz; x++)
algorithm.tex:      if ( !ord[p][C[C[p][q]][q]] ) return(0);
algorithm.tex:and 0 otherwise.  A similar function is easily composed for any other 
algorithm.tex:axiom, just by changing the condition on which to return 0.
algorithm.tex:      if ( C[p][q] == siz ) C[p][q] = 0;
algorithm.tex:      return(0);
algorithm.tex:      FORALL(p) FORALL(q) C[p][q] = 0;
algorithm.tex:   if ( !ord[q][p] )  possval[N[p]][p][q] = 0;
algorithm.tex:or in better C style, since the only values here are 0 and 1,
algorithm.tex:increases to $3^{36}$ or a little over 150,000,000,000,000,000 which 
algorithm.tex:$\C$ & 0 & 1 & 2 & 3 & 4 & 5\\\hline
algorithm.tex:   0 & 5 & 5 & 5 & 5 & 5 & 5\\
algorithm.tex:   1 & 0 & 4 & 4 & 4 & 5 & 5\\
algorithm.tex:   2 & 0 & 3 & 4 & 4 & 4 & 5\\
algorithm.tex:   3 & 0 & 2 & 2 & 4 & 4 & 5\\
algorithm.tex:   4 & 0 & 1 & 2 & 3 & 4 & 5\\
algorithm.tex:   5 & 0 & 0 & 0 & 0 & 0 & 5
algorithm.tex:we have values 5 for \verb|C[p][q]| and 0 for \verb|C[C[p][q]][q]|, 
algorithm.tex:but \verb|ord[1][0]| is 0.  Clearly this badness of the matrix is not 
algorithm.tex:of \verb|<1,4,5>| and \verb|<5,4,0>| is a {\em refutation}.  It is a 
algorithm.tex:           skip = 0;
algorithm.tex:                     <1,4,5>    <5,4,0>  
algorithm.tex:\verb|<5,4>|.  If it inserts any value other than 0 the displayed 
algorithm.tex:refutation is beside the point, but if it inserts 0 then it will go 
algorithm.tex:\verb|<0,0>| up to \verb|<5,3>|, holding \verb|<5,4,0>| fixed, and 
algorithm.tex:its value to something other than 0, 5 is just not a possible value 
algorithm.tex:places it is ``passive".  So before \verb|<5,4,0>| is inserted
algorithm.tex:our sample refutation is active at \verb|<5,4,0>| and passive 
algorithm.tex:this drops to 0 then the entry becomes passive.  The integer 
algorithm.tex:0\ldots\verb|SZ| and sends them to be tested for satisfaction of 
algorithm.tex:chosen subset and 0 everywhere else.  It then returns 0 (FALSE)
algorithm.tex:generate matrices.  In MaGIC 1.0P the master process---the main one 
algorithm.tex:data file in large chunks rather than singly, filling a buffer of 1000 or 
algorithm.tex:$$\begin{picture}(0,12)(0,-6)
algorithm.tex:\put(-8,-4){\line(1,0){16}}
algorithm.tex:\put(-4,3){\line(1,0){11}} \put(-4,5){\line(1,0){11}}
algorithm.tex:\put(-4,-4){\line(0,1){4}} \put(-2,-4){\line(0,1){4}}
algorithm.tex:\put(5,-4){\line(0,1){4}} \put(7,-4){\line(0,1){4}}
algorithm.tex:\put(-1,-4){\line(0,1){2}} \put(1,-4){\line(0,1){2}}
algorithm.tex:\put(2,-4){\line(0,1){6}}  \put(4,-4){\line(0,1){6}}
algorithm.tex:\put(-1,-2){\line(1,0){2}} \put(2,2){\line(1,0){2}}
algorithm.tex:\put(-4,-2){\line(1,0){2}} \put(2,-2){\line(1,0){2}}
algorithm.tex:\put(-4,0){\line(1,0){2}}  \put(2,0){\line(1,0){2}}
algorithm.tex:\put(5,0){\line(1,0){2}}  \put(5,-2){\line(1,0){2}}
algorithm.tex:\put(-6,-3){\line(1,0){2}} \put(-6,-3){\line(0,1){7}}
algorithm.tex:\put(-6,4){\vector(1,0){2}} \put(-3,3){\vector(0,-1){3}}
algorithm.tex:\multiput(-4,3)(2,0){6}{\line(0,1){2}}
algorithm.tex:\put(-2.6,0.5){slave pushes} \put(-2.6,2.1){slave pops}
algorithm.tex:\put(-8,-5){\makebox(0,0){\ldots}} \put(-10,-5){\makebox(0,0){\ldots}}
algorithm.tex:\put(-6,-5){\makebox(0,0){100}} \put(-3,-5){\makebox(0,0){101}}
algorithm.tex:\put(0,-5){\makebox(0,0){102}} \put(3,-5){\makebox(0,0){103}}
algorithm.tex:\put(6,-5){\makebox(0,0){104}}
algorithm.tex:pop from it hangs in a DELAY queue\footnote{{\em ibid}. pp.~20--24} until 
biblio.tex:  {\em Theoretical Computer Science\/} 50 (1987), pp. 1--102.
biblio.tex:   {\em Logique et Analyse\/} 15 (1972), pp.~407--428.
biblio.tex:   Canberra, 1980.
biblio.tex:   {\em Notre Dame Journal of Formal Logic\/} 30 (1989), pp.~117--129.
biblio.tex:   {\em Australasian Journal of Philosophy\/} 68 (1990), pp.~74--88.
biblio.tex:   Technical Report TR-ARP-1/90,
biblio.tex:   Australian National University, Canberra, 1990.
biblio.tex:  Technical Report, forthcoming, Canberra (1990).
biblio.tex:  {\em Proceedings of the 10th International Conference on Automated 
biblio.tex:  Deduction, West Germany, 1990}, forthcoming.
installation.tex:        mstuff/dl.10
installation.tex:        mstuff/dln.10
installation.tex:        mstuff/ln.10
installation.tex:xmagic 1.0 requires MaGIC 1.0; in any case MaGIC must support the $-$x 
installation.tex:version of X Windows (at least X11/R3 for xmagic 1.0 and X11/R4 for xmagic 
installation.tex:At this stage xmagic 1.1 has been tested only on Suns 3/50 and 386i running 
installation.tex:X11/R4 under Sun OS 4.0.3 and (on the 386i) 4.0.1\@.  Xmagic 1.1 has been 
installation.tex:Symmetry S27 with 8 processors running Dynix(R) V3.0.12\@.  The window 
installation.tex:manager used was twm on the 386i and olwm on the 3/50.
mg_header.tex:\topmargin=0mm
mg_header.tex:\textheight=220mm
mg_header.tex:\newcommand{\hugeskip}{\vspace*{10mm}\noindent}
mg_header.tex:\newcommand{\spt}{\raisebox{0.25ex}{$\bullet$}}
mg_header.tex:\def\Dt#1,#2 {\put(#1,#2){\circle*{0.4}}}
mg_header.tex:\def\Diamond#1,#2 {\put(#1,#2){\begin{picture}(0,0)(0,0)
mg_header.tex:  \Dt 2,0 \Dt -2,0 \Dt 0,2 \Dt 0,-2
mg_header.tex:  \Ln -2,0,1,1 \Ln -2,0,1,-1 \Ln 2,0,-1,1 \Ln 2,0,-1,-1
mg_header.tex:\def\Boxx#1,#2 {\put(#1,#2){\begin{picture}(0,0)(0,0)
mg_header.tex:  \Diamond 0,1 \Diamond 0,-1
mg_header.tex:  \Ln 0,1,0,1 \Ln 0,-1,0,-1 \Ln -2,-1,0,1 \Ln 2,-1,0,1
overview.tex:Major \= minor header \= \hs{100mm} \= p\kill
overview.tex:          \> {\bf 5.4} \> Parallelisation                  \> 60 \\[3mm]
overview.tex:          \> {\bf 6.2} \> The R10 and R12 Benchmarks       \> 65 \\[3mm]
overview.tex:The following is a summary of the main differences between versions 1.0 and 
overview.tex:number of processes via menu option `\#'\@.  Unlike MaGIC 1.0P it does not 
overview.tex:than MaGIC 1.0, so it runs over 25\% faster on certain jobs.
overview.tex:Several bugs in 1.0 have been fixed for 1.1\@.  The most important are as 
overview.tex:\item In MaGIC 1.0 the action on satisfaction of user-defined axioms was 
overview.tex:\item MaGIC 1.1, unlike 1.0, stops on time even if no matrices are found.
overview.tex:eliminating isomorphisms than did 1.0\@.  This speeds up execution a little 
overview.tex:GPO Box 4, \ Canberra, \ A.C.T. 2601 \\
results.tex:to the simple affixing fact that if $0\leq 1$ then $5\C 0\leq 5\C 1$\@.  
results.tex:purposes of matrix-generation is the pair of pre-defined axioms 9 and 10:
results.tex:   Matrices &  16 \ & &  70 \ & &   399 \ & &  2261  & & 14358   \\\\
results.tex:{\bf Def 2} &  1.66 & & 14.96 & & 1319.40 & &        & &         \\\\
results.tex:{\bf Def 3} &  0.44 & &  2.72 & &   18.59 & & 531.98 & &         \\\\
results.tex:{\bf Def 4} &  0.41 & &  3.12 & &   18.04 & & 139.18 & & 1066.36 \\\\
results.tex:{\bf Def 5} &  0.38 & &  2.68 & &   13.72 & &  90.54 & & 898.50
results.tex:{\bf Def 5} & & 24 & &  38 & &   34 & & 40  & & 62
results.tex:{\large\bf \S6.2\hs{3mm}The R10 and R12 Benchmarks}
results.tex:all the {\bf R} matrices up to size $10\!\times\!10$ and then up to size 
results.tex:{\bf R10} problem involves generating 742 matrices, in the course of 
results.tex:which 7554 bad ones are tested and 108 isomorphic copies rejected.  For 
results.tex:the {\bf R12} problem there are 4940 good matrices to be found, 54810 bad 
results.tex:ones to be tested and 1109 isomorphs to be omitted.  No file output was 
results.tex:{\bf Table 3: R matrices up to size 10 and size 12}\\[4mm]
results.tex:{\bf R10} time & 123.60 & 62.30 & 41.78 & 31.68 & 26.83 & 23.25 \\
results.tex:        speedup & 1.000 & 1.984 & 2.958 & 3.902 & 4.607 & 5.316 \\\\
results.tex:{\bf R12} time & 1237.6 & 622.8 & 422.0 & 328.0 & 268.4 & 230.0\\
results.tex:        speedup & 1.000 & 1.987 & 2.933 & 3.773 & 4.611 & 5.380
results.tex:It will be seen that the {\bf R12} problem takes almost exactly 10 times 
results.tex:longer than the {\bf R10} problem and that the degree of parallelism 
results.tex:Since only 40720 bad ones are tested along the way, the search ratio is 
results.tex:Sun 3/80 and would have taken close to 50 hours to complete the job.  One 
results.tex:grain size.  Some pieces of work yield over 2000 good matrices while 
results.tex:parameters and once with an expanded heap of 8000 blanks in place of the 
results.tex:default 3500.
results.tex:Normal (sec) & 323.4 & 166.0 & 108.5 & 86.85 & 71.97 & 65.96 \\
results.tex:     speedup & 1.000 & 1.948 & 2.980 & 3.724 & 4.494 & 4.901 \\\\
results.tex: Tuned (sec) & 349.6 & 176.0 & 117.5 & 88.89 & 71.16 & 59.51 \\
results.tex:     speedup & 1.000 & 1.986 & 2.975 & 3.933 & 4.913 & 5.875
results.tex:All of the above benchmarking was done with MaGIC 1.0 and 1.0P\@.  
results.tex:performance of the two releases, but here is a brief report on the {\bf R10} 
results.tex:{\bf Table 5: R10 comparing 1.0P with 1.1P}\\[4mm]
results.tex:{\bf 1.0} time & 123.60 & 62.30 & 41.78 & 31.68 & 26.83 \\
results.tex:       speedup &  1.000 & 1.984 & 2.958 & 3.902 & 4.607 \\\\
results.tex:{\bf 1.1} time &  96.94 & 52.06 & 35.00 & 26.96 & 22.07 \\
results.tex:       speedup &  1.000 & 1.864 & 2.770 & 3.596 & 4.392 \\
results.tex:the percentage increase in speed as MaGIC 1.1 replaces 1.0\@.  The degree of 
results.tex:time taken by MaGIC 1.0 with just one slave.  It may be interesting to note 
user_guide.tex:    Negation table #1   ~ | 0 1 2
user_guide.tex:                          | 2 1 0
user_guide.tex:    Order #1     < | 0 1 2
user_guide.tex:                 0 | + + +
user_guide.tex:    Matrix # 1       -> | 0 1 2
user_guide.tex:                      0 | 2 2 2
user_guide.tex:                      1 | 0 1 2
user_guide.tex:                      2 | 0 0 2
user_guide.tex:elements (2 and 0 in this case) are as always the negations of 
user_guide.tex:total order or chain, with 0 at the bottom, 1 in the middle and 2 
user_guide.tex:$2\C 1$ which is 0, so the bad formula is $1\C 0$ which is 
user_guide.tex:likewise 0.  The runtime statistics this time record that a 
user_guide.tex:we do not wish to set a time limit, so we answer 0 to `how many seconds". 
user_guide.tex:{\bf e}), this time allowing the matrices to get up to size 10 as 
user_guide.tex:After a decent interval (about 50 seconds on our workstation) 
user_guide.tex:MaGIC reports back with a 10$\times$10 matrix, to be found in 
user_guide.tex:{\bf R10.1a2.2} and in \cite{SDM} as {\bf C6}\@.  What you have 
user_guide.tex:matrix, but consider that it had to traverse the 10$\times$10 search 
user_guide.tex:space (na\I vely $10^{100}$ possible matrices) to find this single 
user_guide.tex:To demonstrate the virtues of running MaGIC 1.0P in parallel, we may change 
user_guide.tex:   10   p -> (t -> p)
user_guide.tex:Note that all such definitions are purely abbreviatory: MaGIC 1.0
user_guide.tex:0, 1 or 2.  Any of adicity 0 must be compounded from the sentential 
user_guide.tex:fragments.  For the full logic it is 14 with distribution, 10 
user_guide.tex:it is 10 with distribution, 8 without and 12 with total order; 
user_guide.tex:less than this will be counted as 0\@.  Note that MaGIC may take a 
user_guide.tex:a 60-second run MaGIC may well run for 61.3 seconds or something of 
user_guide.tex:generating as soon as any one of the limits is reached.  Giving 0 as 
user_guide.tex:up to 100 matrices in 30 seconds, but do not care how big they get, you 
user_guide.tex:may take option {\bf e}, specifying the time limit as 30, the maximum 
user_guide.tex:number of matrices as 100 and the size limit as 0.
user_guide.tex:$$\begin{picture}(0,12)(0,-6)
user_guide.tex:\put(-8,3){\vector(1,0){2}}     % into siz
user_guide.tex:\put(-4,3){\vector(1,0){3}}     % siz to ord
user_guide.tex:\put(1,3){\vector(1,0){3}}      % ord to des
user_guide.tex:\put(6,3){\line(1,0){2}} 
user_guide.tex:\put(8,3){\line(0,1){2}} 
user_guide.tex:\put(8,5){\line(-1,0){3}}
user_guide.tex:\put(5,5){\vector(0,-1){1}}     % des to des
user_guide.tex:\put(5,2){\line(0,-1){2}} 
user_guide.tex:\put(5,0){\vector(-1,0){4}}     % des to -1a
user_guide.tex:\put(0,1){\vector(0,1){1}}      % -1a to ord
user_guide.tex:\put(-1,0){\vector(-1,0){3}}    % -1a to -1b
user_guide.tex:\put(-5,1){\vector(0,1){1}}     % -1b to siz
user_guide.tex:\put(-5,-1){\vector(0,-1){1}}   % -1b to -1c
user_guide.tex:\put(-6,-3){\vector(-1,0){2}}   % out from -1c
user_guide.tex:$$\begin{picture}(0,12)(0,-6)
user_guide.tex:\put(-10.5,3){\vector(1,0){2}}    % into siz
user_guide.tex:\put(-6.5,3){\vector(1,0){3}}     % siz to neg
user_guide.tex:\put(3.5,3){\vector(1,0){3}}      % ord to des
user_guide.tex:\put(8.5,3){\line(1,0){2}} 
user_guide.tex:\put(10.5,3){\line(0,1){2}} 
user_guide.tex:\put(10.5,5){\line(-1,0){3}}
user_guide.tex:\put(7.5,5){\vector(0,-1){1}}     % des to des
user_guide.tex:\put(7.5,2){\line(0,-1){2}} 
user_guide.tex:\put(7.5,0){\vector(-1,0){4}}     % des to -1a
user_guide.tex:\put(2.5,1){\vector(0,1){1}}      % -1a to ord
user_guide.tex:\put(1.5,0){\vector(-1,0){3}}     % -1a to -1d
user_guide.tex:\put(-7.5,1){\vector(0,1){1}}     % -1b to siz
user_guide.tex:\put(-7.5,-1){\vector(0,-1){1}}   % -1b to -1c
user_guide.tex:\put(-8.5,-3){\vector(-1,0){2}}   % out from -1c
user_guide.tex:\put(-1.5,3){\vector(1,0){3}}     % neg to ord
user_guide.tex:\put(-3.5,0){\vector(-1,0){3}}    % -1d to -1b
user_guide.tex:\put(-2.5,1){\vector(0,1){1}}     % -1d to neg
user_guide.tex:     1 0
user_guide.tex:     1 1 0 1
user_guide.tex:     2 1 0
user_guide.tex:     1 1 1 0 1 1 0 0 1
user_guide.tex:     3 2 1 0
user_guide.tex:     1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1
user_guide.tex:     1 1 1 1 0 1 1 1 0 0 1 1 0 0 0 1
user_guide.tex:     3 1 2 0
user_guide.tex:     1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1
user_guide.tex:$$\begin{picture}(0,12)(0,-6)
user_guide.tex:\put(-13,3){\vector(1,0){2}}    % into siz
user_guide.tex:\put(-9,3){\vector(1,0){3}}     % siz to neg
user_guide.tex:\put(1,3){\vector(1,0){3}}      % ord to des
user_guide.tex:\put(6,3){\vector(1,0){3}}      % des to aro
user_guide.tex:\put(11,3){\line(1,0){2}} 
user_guide.tex:\put(13,3){\line(0,1){2}} 
user_guide.tex:\put(13,5){\line(-1,0){3}}
user_guide.tex:\put(10,5){\vector(0,-1){1}}     % aro to aro
user_guide.tex:\put(10,2){\line(0,-1){2}} 
user_guide.tex:\put(10,0){\vector(-1,0){4}}     % aro to -1e
user_guide.tex:\put(5,1){\vector(0,1){1}}      % -1e to des
user_guide.tex:\put(4,0){\vector(-1,0){3}}     % -1e to -1a
user_guide.tex:\put(0,1){\vector(0,1){1}}      % -1a to ord
user_guide.tex:\put(-1,0){\vector(-1,0){3}}     % -1a to -1d
user_guide.tex:\put(-10,1){\vector(0,1){1}}     % -1b to siz
user_guide.tex:\put(-10,-1){\vector(0,-1){1}}   % -1b to -1c
user_guide.tex:\put(-11,-3){\vector(-1,0){2}}   % out from -1c
user_guide.tex:\put(-4,3){\vector(1,0){3}}     % neg to ord
user_guide.tex:\put(-6,0){\vector(-1,0){3}}    % -1d to -1b
user_guide.tex:\put(-5,1){\vector(0,1){1}}     % -1d to neg
user_guide.tex:  hscale=0.75
user_guide.tex:  vscale=0.75 }
user_guide.tex:constant in a 10-element structure, however, it should be possible to 
user_guide.tex:the bound 0 here is equivalent to disabling this option.  See MaGIC 
user_guide.tex:any case when the file is exhausted.  As for MaGIC, giving the bound 0