Package FAtiMA.Core.wellFormedNames

Class Unifier

java.lang.Object

FAtiMA.Core.wellFormedNames.Unifier

public abstract class Unifier
extends java.lang.Object

Static Class that implements the Unifying algorithm

Author:

Joao Dias

Constructor Summary

Constructors

Constructor	Description
Unifier()

Method Summary

Modifier and Type	Method	Description
static java.util.ArrayList<Substitution>	Unify(Name n1, Name n2)
static boolean	Unify(Name n1, Name n2, java.util.ArrayList<Substitution> bindings)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Unifier

public Unifier()

Method Detail

Unify

public static boolean Unify(Name n1,
                            Name n2,
                            java.util.ArrayList<Substitution> bindings)

Parameters:

n1 - - The first Name

n2 - - The second Name

bindings - - Place an empty Substitution List here

Returns:

True if the names are unifiable, in this case the bindings list will contain the found Substitutions, otherwise it will be empty

See Also:

Name, Unifying Method, receives two WellFormedNames and tries to find a list of Substitutions that will make both names syntatically equal. The algorithm does not perform Occur Check, since the unification of [X] and Luke(Strength) is allways assumed to fail. The method goes on each symbol (for both names) at a time, and tries to find a substitution between them. Take into account that the Unification between [X](John,Paul) and Friend(John,[X]) fails because the algorithm considers [X] to be the same variable

Unify

public static java.util.ArrayList<Substitution> Unify(Name n1,
                                                      Name n2)

Parameters:

n1 - - The first Name

n2 - - The second Name

Returns:

A list of substitutions if the names are unifyable, otherwise returns null

See Also:

Name, Unifying Method, receives two WellFormedNames and tries to find a list of Substitutions that will make both names syntatically equal. The algorithm does not perform Occur Check, since the unification of [X] and Luke(Strength) is allways assumed to fail. The method goes on each symbol (for both names) at a time, and tries to find a substitution between them. Take into account that the Unification between [X](John,Paul) and Friend(John,[X]) fails because the algorithm considers [X] to be the same variable