// 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