First it says "== unifies two terms". Then the first example says "(== x z) (== 3 y)" associates x with z and y with 3. Are "unify" and "associate" the same thing? Why use different words? Why does the association reverse for x and z vs 3 and y? Is it commutative?
(== x x) = x for all x
(== x y) = (== y x) for all x and y
(== x (== x y)) = (== x y) for all x and y
(== x (== y z)) = (== (== x y) z)
(== [x, 1] [2, y]) = [2, 1]
(== [2, y] [z, 3]) = [2, 3]
(== [x, 1] [z, 3]) does not unify (since 1 does not unify with 3)From the submitted page, "The core language, using Scheme as the host language, is described in this short, interactive tutorial."
Really---anything short of that is sub-optimal performance. I think some of it comes from new eyes reading and pointing out room for improvement. The other half is someone having the time to figure out the fix and implement it.
For example you could start with two facts like "Fedora is red." and "Cat is green." Then if you ask the system "X is red." it'll tell you "X = fedora". If you ask it to list all the solutions of "X and Y are not the same color." it'll list "X = fedora, Y = cat" and "X = cat, Y = fedora". This process of binding variables to values (or other variables during simplification) is unification.