I need a working code in either c++/java for the unify with occurs check as in prolog. it should have the following test cases satisfied.

p.s: I strictly need the code in either C++/ Java.

Thanks in advance.

Unification is the process where the interpreter takes two terms and defines an term that satisfies them both. Practically speaking this means the interpreter must assign values to variables in the two descriptions to make them match.

For example, if one term is f(X, Y) and the second is f(g(Y, a), h(a)) (where upper case names are variables and lower case are constants) then the two terms can be unified by identifying X with g(h(a), a) and Y with h(a) making both terms look like f(g(h(a), a), h(a)). The unification can be represented by a pair of substitutions {X -> g(h(a), a)} and {Y -> h(a)}. An algorithm for unification appears below.

Divide your solution into the following parts:

PART I: Substitution

A substitution is a mapping from from variables to terms. I will call each variable/term pair a "correspondence". There are several ways to represent a correspondence in PROLOG, such as a list of length two where the first element of the list is a variable and the second element is the term, or a functor with two components labeled "variable" and "term". Once you have chosen a representation for a correspondence, then you can represent a substitution as a list of correspondences. You should provide a set of rules for treating substitutions as an abstract data type. You should have rules to provide the following capabilities:

Define a new (empty) substitution

Add a correspondence to a substitution

Check whether a particular variable is the first member of any correspondence in a substitution and return the second member

Compose two substitutions to get a third

Apply a substitution to a term

PART II: Unification

Unification makes heavy use of substitution. For this part of the assignment, you should implement the unification algorithm described below, including the occurs check. In addition to constructing the unifying substitution (or failing where appropriate), your rules should print out the result of applying the substitution to the two terms being unified.

Using C++ (or any other language as long as it compiles runs on hercules with the UNIX system), implement the unification algorithm seen in class. Your program should have the same behavior as the unify_with_occurs_check(termi,term2) build-in predicate of Gnu Prolog. term I and term2 are 2 terms where variables are in upper case letters. Function symbols are in lower case letters. Examples: 12- unify_with_occurs_check(a,x). X= a yes |?- unify_with_occurs_check(X,Y). Y = X yes |?- unify_with_occurs_check(X,f(Y)). X=f(Y) yes |?- unify_with_occurs_check(X,h(a, Y)). X=h(a, Y) yes |?- unify_with_occurs_check(f(f(X,Y),X),f(f(V,U),g(U,Y))). V= g(U,U) X= g(UU) Y= U Using C++ (or any other language as long as it compiles runs on hercules with the UNIX system), implement the unification algorithm seen in class. Your program should have the same behavior as the unify_with_occurs_check(termi,term2) build-in predicate of Gnu Prolog. term I and term2 are 2 terms where variables are in upper case letters. Function symbols are in lower case letters. Examples: 12- unify_with_occurs_check(a,x). X= a yes |?- unify_with_occurs_check(X,Y). Y = X yes |?- unify_with_occurs_check(X,f(Y)). X=f(Y) yes |?- unify_with_occurs_check(X,h(a, Y)). X=h(a, Y) yes |?- unify_with_occurs_check(f(f(X,Y),X),f(f(V,U),g(U,Y))). V= g(U,U) X= g(UU) Y= U