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