CSCI 485 --- Fall 2023

Lab 8

Problem Description:

Unification is a process of making two first order logic sentences with universal quantified variables identical by finding a substitution.

When two FOL sentences are standardized variables apart, there is a single most general unifier (MGU) that is unique up to renaming of variables.

The unification algorithm for two atomic FOL sentences is shown below:

// substituteSet is empty to start with
// and empty substituteSet is not failure
// S1 can be a variable, constant, predicate or function
// S2 can be a variable, constant, predicate or function
function unify(S1, S2, substituteSet) returns a substitution or failure
{
    if (substituteSet == failure)
        return failure; // empty_set is not a failure
    else if (S1 == S2) {
        return substituteSet;
    else if (S1 is variable)
        return unifyVar(S1, S2, substituteSet);
    else if (S2 is variable)
        return unifyVar(S2, S1, substituteSet);
    else if (S1 and S2 are both predicates or functions) {
        // header(S1) gives back S1's predicate symbol or function symbol
	if (header(S1) == header(S2)) {
            list1 = S1's arguments
            list2 = S2's arguments
            if (list1.size == list2.size) {
                for(int i = 0; i < list1.size; i++) {
                    unify(list1.element(i), list2.element(i), substituteSet);
                    if (subsituteSet == failure)
                        return failure;
                }
                return substituteSet;
            } else {
                return failure;
            }
        } else {
            return failure;
        }
    } else {
        return failure;
    }
}

// x is a variable
// y is an expression (constant, variable, or function)
function unifyVar(x, y, substituteSet) // substituteSet pass by reference
{
    if ((x/val) is in substituteSet)
        return unify(val, y, substituteSet);
    else if ((y/val) is in substituteSet);
        return unify(x, val, substituteSet);
    else if (x occures in the expression y)
        return failure;
    else
        return (substituteSet union {x/y});
}

Your Task:

You can make the following assumptions:

• Constants are marked with a pare of single quotation marks;
• Predicate symbols, function symbols and variables only contain letters and digits;
• Variables always start with a lower case letter;
• Predicate symbols and function symbols always start with an upper case letter.

Implement this unification function. And try to unify the following two expressions and display your unification result:

Colleagues(x, Instructor('BIOL 490', y))
Colleagues(Instructor('BIOL 121', 'Fall 2023'), z)