Leaf Rules: are they variables or constant values?

The Unification Algorithm has an interesting property is that it doesn't matter whether a leaf rule is really a variable or a fact/a constant (a rule without arguments). John could be a constant or a variable. The unification doesn't care. Only the structure (are there arguments and how many?) is important.

But usually one wants to substitute only variables and not constants. It doesn't make sense to substitute the constant value John with another constant value James.

Unification modes

Therefore the Unification Algorithm presented here has two modes:

• Use variables and values
• Use only variables

In the first modus one-letter leaf rules (like x) are interpreted as variables. Other leaf rules (like John) are constants and never substituted.

In the second mode all leaf rules can be substituted with each other. Unification of Knows(John,Mary) and Knows(James,Mary) results in the substitution {John/James}.

Back to the page "Unification Algorithm"