*** Running FFF... *** Run of Sat Sep 15 11:00:09 CEST 2018 *** *** Welcome to FFF, a facility (under development) for fuzzy lattice operations on first-order terms *** *** Type '#help;' for help or 'quit;' to quit (if no prompt upon an error, type ';') *** FFF> #load "slidesex.fff"; #load "slidesex.fff"; FFF> #fun a/0 b/0 c/0 d/0 f/2 g/2 h/3; *** The current signature has 7 functors: {a/0, b/0, c/0, d/0, f/2, g/2, h/3} FFF> #sim a b 0.7 c d 0.6 f g 0.9; *** Declared similarities: a b 0.7 c d 0.6 f g 0.9 FFF> #close; *** Computed similarity closure (enter '#show;' to see it) FFF> h(f(a,X1),g(X1,b),f(Y1,Y1)) \/ h(X2,X2,g(c,d)); @@@ generalizing lhs term h(f(a,X1),g(X1,b),f(Y1,Y1)) and rhs term h(X2,X2,g(c,d)) at degree 1.0 @@@ argument 1 @@@ unapplying left substitution {} and right substitution {} to lhs term f(a,X1) and rhs term X2 at degree 1.0 @@@ there is no similar unapplication for f(a,X1) and X2 at degree 1.0 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 2 @@@ unapplying left substitution {_0=f(a,X1)} and right substitution {_0=X2} to lhs term g(X1,b) and rhs term X2 at degree 1.0 @@@ the lhs argument 0's unapplied variable _0 gives term: f(a,X1) resulting in degree 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: X2 resulting in degree 1.0 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for g(X1,b) and X2 at degree 1.0 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 3 @@@ unapplying left substitution {_0=f(a,X1), _1=g(X1,b)} and right substitution {_0=X2, _1=X2} to lhs term f(Y1,Y1) and rhs term g(c,d) at degree 1.0 @@@ the lhs argument 0's unapplied variable _0 gives term: f(a,X1) resulting in degree 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ the lhs argument 1's unapplied variable _1 gives term: g(X1,b) resulting in degree 0.0 @@@ the rhs argument 1's unapplied variable _1 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for f(Y1,Y1) and g(c,d) at degree 1.0 @@@ the final unapplied fuzzy pair is the original unchanged @@@ generalizing lhs term f(Y1,Y1) and rhs term g(c,d) at degree 1.0 @@@ since f ~ g [0.9] the new generalization degree is now 0.9 @@@ argument 1 @@@ unapplying left substitution {_0=f(a,X1), _1=g(X1,b)} and right substitution {_0=X2, _1=X2} to lhs term Y1 and rhs term c at degree 0.9 @@@ the lhs argument 0's unapplied variable _0 gives term: f(a,X1) resulting in degree 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ the lhs argument 1's unapplied variable _1 gives term: g(X1,b) resulting in degree 0.0 @@@ the rhs argument 1's unapplied variable _1 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for Y1 and c at degree 0.9 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 2 @@@ unapplying left substitution {_0=f(a,X1), _2=Y1, _1=g(X1,b)} and right substitution {_0=X2, _2=c, _1=X2} to lhs term Y1 and rhs term d at degree 0.9 @@@ the lhs argument 0's unapplied variable _0 gives term: f(a,X1) resulting in degree 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ the lhs argument 1's unapplied variable _1 gives term: g(X1,b) resulting in degree 0.0 @@@ the rhs argument 1's unapplied variable _1 gives term: X2 resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ the lhs argument 2's unapplied variable _2 gives term: Y1 resulting in degree 1.0 @@@ the rhs argument 2's unapplied variable _2 gives term: c resulting in degree 0.6 @@@ so the resulting unapplication degree is 0.6 @@@ therefore the final unapplied fuzzy pair is <_2,_2,0.6> *** The fuzzy lub is h(_0,_1,f(_2,_2)) *** Its approximation degree is 0.6 *** Its 0.6-similar term representative is h(_0,_1,f(_2,_2)) *** Left substitution: *** _0 = f(a,X1) *** _1 = g(X1,b) *** _2 = Y1 *** Right substitution: *** _0 = X2 *** _1 = X2 *** _2 = c FFF> f(Y1,Y1) \/ g(c,d); @@@ generalizing lhs term f(Y1,Y1) and rhs term g(c,d) at degree 1.0 @@@ since f ~ g [0.9] the new generalization degree is now 0.9 @@@ argument 1 @@@ unapplying left substitution {} and right substitution {} to lhs term Y1 and rhs term c at degree 0.9 @@@ there is no similar unapplication for Y1 and c at degree 0.9 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 2 @@@ unapplying left substitution {_0=Y1} and right substitution {_0=c} to lhs term Y1 and rhs term d at degree 0.9 @@@ the lhs argument 0's unapplied variable _0 gives term: Y1 resulting in degree 1.0 @@@ the rhs argument 0's unapplied variable _0 gives term: c resulting in degree 0.6 @@@ so the resulting unapplication degree is 0.6 @@@ therefore the final unapplied fuzzy pair is <_0,_0,0.6> *** The fuzzy lub is f(_0,_0) *** Its approximation degree is 0.6 *** Its 0.6-similar term representative is f(_0,_0) *** Left substitution: *** _0 = Y1 *** Right substitution: *** _0 = c FFF>