Matching in Artificial intelligence, unification

Question

trying to implement matching which is a limited form of unification.

trying to match two formulas match if we can find substitutions for the variables appearing in the formulas such that the two are syntactically equivalent.

I need to write a function that determines whether a constant corresponding to a ground term such as Brother(George) and a pattern corresponding to a quantified formula such as Brother(x) match. If they do match the function returns a set of substitutions called bindings that map variables to terms. A constant matches another constant if they are equal. An unbound variable (one currently without a binding) matches any formula. A bound variable matches a constant if the constant and the value to which the variable is bound are equal.

examples:

match( Loves(Dog(Fred), Fred)

Loves(x,y))

is true with x = Dog(Fred) and y = Fred

another one

match( Loves(Dog(Fred), Fred)

Loves(x,x)

fails

Answer 1

The concept of MGUs i.e. Most General Unifiers seems to be of use over here. The solution methodology is illustrated below.
Let us have an initial empty set named mgu and another empty set E.

mgu = {}
G = match(Loves(Dog(Fred),Fred),Loves(x,y))
E = {Loves(Dog(Fred),Fred),Loves(x,y)}


mgu = {Fred|y}             // Replace Fred by y, variables to be replaced first.
G = match(Loves(Dog(y),y),Loves(x,y))
E = {Loves(Dog(y),y),Loves(x,y)}


mgu = {Fred|y,Dog(y)|x}    // Replace Dog(y) by x
G = match(Loves(x,y),Loves(x,y))  
E = {Loves(x,y)}           // E becomes a singleton set here, we stop here.
                           // No more substitutions are possible at this stage.

match() returns True if E becomes a singleton set when no more substitutions are possible, otherwise False. And the mgu can be returned as the set of substitutions required.

G = True
mgu = {Fred|y,Dog(y)|x}

The other example can be illustrated as follows.

mgu = {}
G = match(Loves(Dog(Fred),Fred),Loves(x,x))
E = {Loves(Dog(Fred),Fred),Loves(x,x)}


mgu = {Fred|x}             // Replace Fred by x.
G = match(Loves(Dog(x),x),Loves(x,x))
E = {Loves(Dog(x),x),Loves(x,x)}


mgu = {Fred|x,Dog(x)|y}       // Replace Dog(x) by y
G = match(Loves(y,x),Loves(x,x))  
E = {Loves(y,x),Loves(x,x)}   // E does not becomes a singleton set here.
                              // But no more substitutions are 
                              // possible at this stage.

Therefore,

G = False