Unification Rules

Unification rules
A constant unifies only with itself.
Two structures unify if and only if they have the same functor and the same number of arguments, and the corresponding arguments unify recursively.
A variable unifies with anything.
Unification = Matching + Occurs check
What happens when we ask Prolog:
?- X = f(X).
Matching succeeds, unification fails

Rules

Prolog clauses such as:
“offspring(Y,X):-parent(X,Y).” are called rules.
There is difference between facts and rules.
Fact syntax and the meaning:
parent(tom,liz).
Rule has two parts a condition (head) and a conclusion part (body).