// connection graph proof procedure / R. Kowalski, Logic for Problem Solving, North Holland, 1979 // unification / A. Martelli & A. Montanari, An Efficient Unification Algorithm, / ACM Transactions on Programming Languages and Systems, 4(2), 1982 V:`x`y`z`u`v`w / variable symbols v:{x _in V} / x a variable? unify:{:[x~y;();x[0]=*y;(vt fg tv vv tt@)/+(1_ x;1_ y)]} / find most general unifier (or _n) tt:{:[@x;;_di[x;i],,/(+1_')'x i:&{:[|/@:'x;0;~=/#:'x;0;=/*:'x]}'x]} / [f T][f U] -> +[T U] vv:{:[@x;;x _di&{(&/v'x)&~/x}'x]} / v v -> tv:{:[@x;;{( v t fg:{:[@x;;~|/{:[|/v'x;0;~~/*:'x]}'x;x]} / [f T][g T] -> FAIL / ff:{:[@x;;~|/{:[~=/*:'x;0;~=/#:'x]}'x;x]} / [f T][F U], ~(#T)=#U, -> FAIL (special case) vt:{ / v t -> replace :[@x ; / FAIL? ~#i:&{>/v'x}'x ;x / v t ~#i@:&x[i;0](|/occurs/:)'x _di/:i ;x / v occurs elsewhere ~|/occurs .'x i ;replace/[x;i]]} / v occurs in self -> FAIL else replace replace:{apply[x _di y;x y],,x y} / replace v from v t elsewhere apply:{:[~@x;x _f\:y;x=*y;y 1;x]} / apply y=[.. v t ..] in x occurs:{:[@y;x=y;|/x _f/:y]} / v occurs in E A:((();,`Happy`u) (,`Happy`x;,`Playing`x) (,`Happy`x;(`Working`y;`Employs`x`y)) ((`Playing`bob;`Working`bob);()) (,`Employs`john`bob;())) connect:{[p](,/,/,/(!#p)links[p]/:\:!#p)_dv()} links:{[p;i;j](!#p[i;0])link[p;i;j]/:\:!#p[j;1]} link:{[p;i;j;k;l]:[_n~u:unify[p[i;0;k];p[j;1;l]];();(i;j;k;l;u)]}