// tabular logic // box notation L:{.+(`v`h`bl;x)}'3 3#"\263\304\300\263\304\300\272\315\310" / box characters rep:{:[@x;,1!" ",\$x;1=#x;enc[L t;_f(1|t:typ x)*:/x];hor/_f'x]} / represent (2 symbols) / rep:{:[@x;,1!" ",\$x;1=#x;t enc[*L]/_f(t:1|typ x)*:/x;hor/_f'x]} / represent (1 symbol) enc:{(((#y)#x`v),x`bl),'y,,((^y)1)#x`h} / enclose hor:{m:(#x)|#y;pad[x;m],'pad[y;m]} / glue horizontal pad:{x,((y-#x),(^x)1)#" "} / pad with blanks ver:{+hor[+x;+y]} / glue vertical // conjunctive normal form anno:{:[~x;20#"";"(",(" ~";"~~")[-1+*x],") C:",(-2\$y)," R:",(-2\$z),4#" "]} / annotate cnf step diagram:{hor[,anno . 3#y;grid x]} / diagram matrix cnf:{`0:,/(diagram .)'-1_ r:(red .)\(,:''x;!0);`0:,20#"-";`0:grid r:cmp@**|r;r} / reduce to cnf cmp:{?({x@ ,x and:(::) / ..&x&..-> ..x.. or:{not and@not'x} / ..|x|.. -> ,..(,x).. onlyif:{not and(x;not y)} / x->y -> ,(x;,y) iff:{and(onlyif[x;y];onlyif[y;x])} / x<->y -> (x->y)&y->x p:`p;q:`q;r:`r;s:`s;t:`t / propositional symbols false:not true:` / truth constants // elimination rules red:{y;:[(#x)=i:(|/'0 (`p;,`r;`s) neg:{:[@x;,x;*x]} / `p <-> ,`p clash:{(#x),/:&x{|/x _lin y}\:neg'y} / clauses in x which clash with y // represent, display dsp:{[c;i]line[c]'[!#i;i];c} / display proof line:{[c;k;i]`0:,"";`0:hor[fmt[k;i];:[#c k;grid@,c k;,""]]} / line of proof fmt:{[k;i],(-5\$k),:[@i;15#" ";(,/-5\$i),5#" "]} / format annotation // examples a:onlyif[onlyif[p;q];onlyif[not q;not p]] b:cnf a c:(,,`r;(`p;`q;,`q);`p`q;`p`r;(,`p;`r);`r`s;(`r;,`q);(,`s;,`q)) d:(`r`p;(,`r;`p);(,`q;,`p);(`q;,`p)) prove[sat;c] prove[sat;d]