Unification&Proof search

一、Unification

1,Definition

– two terms unify: •  if they are the same term, or •  if they contain variables that can be uniformly instantiated with terms in such a way that the resulting terms are equal 2,how -- If T1 and T2 are constants, then T1 and T2 unify if they are the same atom, or the same number   --T1 is a variable and T2 is any type of term, then T1 and T2 unify, and T1 is instantiated to T2 (and vice versa) 3.  If T1 and T2 are complex terms then they unify if: 1.  They have the same functor and arity, and

2.  all their corresponding arguments unify, and

3.  the variable instantiations are compatible Eg

?- X=mia, X=vincent. no
Prolog has instantiated X with mia, so that it cannot unify it with vincent anymore

Which of the following pairs of terms unify?

3,Occurs Check

Prolog does not use a standard unification algorithm

?- father(X) = X.
X=father(father(father(…)))) yes

A standard unification algorithm carries out an occurs check •  If it is asked to unify a variable with another term it checks whether the variable occurs in this term •  In Prolog (ISO standard):

?- unify_with_occurs_check(father(X), X). no

4,eaxmple

house_elf(dobby). witch(hermione). witch("McGonagall"). witch(rita_skeeter). magic(X):- house_elf(X). magic(X):- witch(X).
?-magic(Hermione). Hermione = dobby Hermione = hermione Hermione = "McGonagall" Hermione = rita_skeeter

二、Search trees

1,

2,

loves(vincent,mia). loves(marsellus,mia). jealous(A,B):- loves(A,C), loves(B,C).
?-jealous(X,Y).
X = Y, Y = vincent X = vincent, Y = marsellus X = marsellus, Y = vincent X = Y, Y = marsellus