# 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*}.