// tabular logic // box notation R:1 / 2=use line-drawing chars L2:{.+(`v`h`bl;x)}'3 3#"\263\304\300\263\304\300\272\315\310" / line-drawing characters L1:.+(`v`h`bl;"|-+") / |-+ rep:{:[@x;,1!" ",$x;1=#x;:[R=1;rep1;rep2]x;hor/_f'x]} / represent rep2:{enc[*L2 t;rep(1|t:typ x)*:/x]} / represent (2 symbols) rep1:{t enc[L1]/rep(t:1|typ x)*:/x} / represent (1 symbol) enc:{(((#y)#x`v),x`bl),'y,,((^y)1)#x`h} / enclose hor:{m:(#x)|#y;pad[x;m],' :[~/(*|^:)'(x;y);" ";""],/: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:sep 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]