// 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'x)!x}'x]}						/ t v -> 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)]}