// resolution theorem prover (propositional calculus) // strategies sat:{z} / level saturation sup:{z@&|/+{:[~@x;1;|/~x]}''y z} / set of support upr:{z@<#:''x z} / unit preference // resolution / s = strategy (function) / p = premise-set, p 0 = goal clause / q = propositional symbols (string) / c = list of clauses (proof so far) / i = indices into c (justification so far) / j = indices into c (resolvents to process) / r = current resolvent / k = index of current resolvent prove:{[s;p]~#*|r0[s;p;?(,/p)_dvl" -"]} / p unsatisfiable iff proof ends in !0 r0:{[s;p;q]dsp[q]. r1[s;,/tautology'rep[q;p]]} / represent, delete tautologies, refute, display r1:{[s;c]r2[s;c;!#c]} / initialize: base set indices r2:{[s;c;i]r3[s;c;i;s[c;i;,/((1_ i)#\:c)clash'1_ c]]1 2} / initialize: resolvents to process r3:{[s;c;i;j]{(#x 3)&&/#:'x 1}{r4 . x}/(s;c;i;j)} / resolve while more resolvents and no contradiction r4:{[s;c;i;j]r5[s;c;i;1_ j;*j;resolve . c j 0]} / try to resolve next pair of clauses r5:{[s;c;i;j;k;r]:[r _in c;(s;c;i;j);r7[s;c,,r;i,,k;r6[c;j;r]]]} / append resolvent r6:{[c;j;r]:[#r;j,clash[c;r];j]} / clashes if r not null r7:{[s;c;i;j](s;c;i;s[c;i;j])} / apply strategy tautology:{:[(#x)=#?_abs x;,x;!0]} / e.g. 1 2 3 -2 resolve:{?_dvl[x;-y],_dvl[y;-x]} / e.g. 1 2 -3, -2 1 3 5 -> 1 5 clash:{(#x),/:&x{|/x _lin y}\:-y} / clauses in x which clash with y // represent, display rep:{[q;p]p{(),._ssr/[x;q;y]}\:(\$1+!#q),'" "} / symbols -> indices dsp:{[q;c;i]({`0:,(5\$x),:[@z;10\$" ";,/5\$z],,/5\$q fmt/:y}').(!#c;c;i);c} / show proof as table fmt:{[q;c]:[c<0;"-";""],q -1+__abs c} / indices -> symbols // example p:("-r";"pq-q";"pq";"pr";"-pr";"rs";"r-q";"-s-q") q:("rp";"-rp";"-q-p";"q-p") `0:,"level saturation:" prove[sat;p] `0:,"set of support:" prove[sup;p] `0:,"unit preference:" prove[upr;p] `0:,"not a theorem:" prove[sat;(,"q";"pq";"-p")] // explicit version of prove Prove:{[s;p] q:?(,/p)_dvl" -" c:,/tautology'rep[q;p] i:!#c j:s[c;i;,/((1_ i)#\:c)clash'1_ c] while[(#j)&&/#:'c k:*j j:1_ j r:resolve . c k if[~r _in c c,:,r i,:,k if[#r;j:s[c;i;j,clash[-1_ c;r]]]]] dsp[q;c;i] ~#*|c} \ proof = [line#, left parent line#, right parent line#, result clause ..] level saturation: 0 -r 1 p q 2 p r 3 -p r 4 r s 5 r -q 6 -s -q 7 2 0 p 8 3 0 -p 9 3 1 r q 10 3 2 r 11 4 0 s 12 5 0 -q 13 5 1 r p 14 6 1 -s p 15 6 4 -q r 16 8 1 q 17 8 7 1 set of support: 0 -r 1 p q 2 p r 3 -p r 4 r s 5 r -q 6 -s -q 7 2 0 p 8 3 0 -p 9 4 0 s 10 5 0 -q 11 7 3 r 12 8 1 q 13 8 7 1 unit preference: 0 -r 1 p q 2 p r 3 -p r 4 r s 5 r -q 6 -s -q 7 2 0 p 8 7 3 r 9 8 0 1 not a theorem: 0 q 1 p q 2 -p 0