First-order unification
First-order logic adds objects, predicates, functions, and variables to propositional logic, so it can say, for example, that everyone who knows John likes him. To apply a rule such as Knows(John, x) to a fact such as Knows(y, Mary), an inference system must find a substitution for the variables that makes the two expressions identical. Finding it is called unification, and the substitution is a unifier. A most general unifier (MGU) is the least restrictive one; for example, x = Mary and y = John unifies the two sentences above.
Python
def is_variable(term):
return isinstance(term, str) and term[:1].islower()
def occurs(var, term, theta):
if var == term:
return True
if is_variable(term) and term in theta:
return occurs(var, theta[term], theta)
if isinstance(term, tuple):
return any(occurs(var, item, theta) for item in term)
return False
def unify_var(var, term, theta):
if var in theta:
return unify(theta[var], term, theta)
if is_variable(term) and term in theta:
return unify(var, theta[term], theta)
if occurs(var, term, theta):
return None
return {**theta, var: term}
def unify(x, y, theta):
if theta is None:
return None
if x == y:
return theta
if is_variable(x):
return unify_var(x, y, theta)
if is_variable(y):
return unify_var(y, x, theta)
if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
for a, b in zip(x, y):
theta = unify(a, b, theta)
return theta
return None
print(sorted(unify(("Knows", "John", "x"), ("Knows", "y", "Mary"), {}).items()))
print(unify(("P", "x"), ("P", ("F", "x")), {}))
print(unify(("Knows", "John"), ("Likes", "John"), {}))
print(sorted(unify(("P", "x", "x"), ("P", "y", "Z"), {}).items()))