// resolution theorem prover

\l unify

// strategies

upr:{[c;h;i;j]j@<#:''c@2#'j}						/ unit preference
sup:{[c;h;i;j]j@&|/+{:[~@x;1;x<h]}''i 2#'j}				/ set of support
control:{[c;h;i;j]upr[c;h;i;sup[c;h;i;j]]}				/ combined control regime

// resolution

/ g = goal-set
/ p = premise-set
/ c = list of clauses (proof so far)
/ h = # goal clauses
/ i = indices into c (justification so far)
/ j = indices into c (clauses to process)
/ r = current resolvent
/ k = index of current resolvent

prove:{[g;p]p0[g,p;#g;!#g,p]}						/ p unsatisfiable iff proof ends in ()
p0:{[c;h;i]p1[c;h;i;control[c;h;i;,/((1_ i)#\:c)clash'1_ c]]0 2}	/ initialize clauses to process
p1:{[c;h;i;j]{(#x 3)&&/#:'x 0}{p2 . x}/(c;h;i;j)}			/ continue while more to process and no contradiction
p2:{[c;h;i;j]p3[c;h;i;1_ j;*j;resolve[c;*j]]}				/ try to resolve next pair of clauses
p3:{[c;h;i;j;k;r]:[r _in c;(c;h;i;j);p4[c,,r;h;i,,k;p5[c;j;r]]]}	/ append resolvent
p4:{[c;h;i;j](c;h;i;control[c;h;i;j])}					/ apply control regime
p5:{[c;j;r]:[#r;j,clash[c;r];j]}					/ clashes if r not null

/ operations

resolve:{?,/apply/[(x[y 0]_di y 2;x[y 1]_di y 3);y 4]}			/ resolve two clauses
clash:{,/((#x),/:!#x),/:'x match\:negate'y}				/ clauses in x which clash with y
match:{j@:i:&(#x)>j:x[;0]?/:y[;0];+(i;j;u)@\:&~@:'u:x[j]unify'y i}	/ match indices and mgu
negate:{@[x;0;~:]}							/ negate predicate symbols

/ deletions

subsumes:{|/(x;y){&/_lin/apply/[x;y]}/(,/x unify/:\:y)_dv _n}		/ x subsumes y?
tautology:{|/x _lin negate'x}						/ x a tautology?
true:{}									/ procedural attachment

/ answer extraction

answer:{[g;p]a0[g;p]. prove[g;p]}					/ extract a single answer
a0:{[g;p;c;i]:[~#*|c;a1/[a2'[g],p;(#g,p)_ i]]}				/ if proveable, apply proof to goal tautologies
a1:{[d;i]d,,resolve[d;i]}						/ apply next proof-step
a2:{[g]g,:[1=#g;(),;`AND,,:]@negate'g}					/ goal -> goal or ~goal

// examples

G:,(`i.`Z;`r`Z)
P:((`r.`X;`l`X)
   (`d.`Y;`l.`Y)
   ,`d`a
   ,`i`a)

`0:,"single goal:"
prove[G;P]

// She's a witch! Burn her! Proof by Resolution Theorem Proving
// ji@close.cs.columbia.edu (John Ioannidis)
// Columbia University Department of Computer Science
/
/ burns(x) & woman(x) -> witch(x)
/ woman(girl)
/ (x) madeOfWood(x) -> burns(x)
/ (x) floats(x) -> madeOfWood(x)
/ floats(duck)
/ (x)(y) floats(x) & sameWeight(x,y) -> floats(y)
/ sameWeight(duck,girl)
/ ---
/ witch(girl)

G:,,`witch.`girl
P:((`burns.`X;`woman.`X;`witch`X)
   ,`woman`girl
   (`madeOfWood.`X;`burns`X)
   (`floats.`X;`madeOfWood`X)
   ,`floats`duck
   (`floats.`X;`sameWeight.`X`Y;`floats`Y)
   ,`sameWeight`duck`girl)

`0:,"she's a witch!"
prove[G;P]

G:((`b.`X;`c.`X)
   (`b.`X;`d.`X))

P:((`a.`X;`f`X;(`g;`foo`X))
   (`f.`X;`b`X)
   (`f.`X;`c`X)
   (`g.`X;`b`X)
   (`g.`X;`d`X)
   ((`a;`goo`X);(`f;`hoo`X)))

`0:,"multiple goals:"
prove[G;P]

`0:,"extract an answer:"
answer[G;P]