// 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;xj: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]