The Most General Unifier (MGU): Foundation of Automated Reasoning

Introduction

When automated theorem provers work with first-order logic, they frequently need to determine whether two logical expressions can be made identical through variable substitutions. This process—unification—is fundamental to virtually every automated reasoning system. At the heart of unification lies a crucial concept: the Most General Unifier (MGU).

The MGU represents the most general substitution that makes two terms identical, without imposing unnecessary constraints. Understanding MGU is essential for anyone working with logic programming languages like Prolog, resolution-based theorem provers, type inference systems, or any application requiring pattern matching with variables.

This article provides a comprehensive introduction to MGU, explaining what it is, why it matters, how to compute it, and where it appears in practice.

Understanding Unification

The Basic Idea

Unification is the process of finding a substitution for variables that makes two logical terms identical. A substitution is a mapping from variables to terms.

Consider these terms:

• $P(x, f(y))$
• $P(a, f(z))$

Can we find a substitution that makes them equal? Yes: $\{x/a, y/z\}$

After applying this substitution:

• $P(x, f(y))\{x/a, y/z\} = P(a, f(z))$

The terms unify!

Formal Definition

Given two terms $t_1$ and $t_2$, a unifier is a substitution $\sigma$ such that:

Where $t\sigma$ denotes applying substitution $\sigma$ to term $t$.

Types of Terms

First-order terms come in several forms:

What Makes a Unifier “Most General”?

The Key Insight

Multiple unifiers may exist for the same pair of terms. Consider:

Terms: $P(x)$ and $P(f(y))$

Possible unifiers:

1. $\{x/f(y)\}$ — directly substitutes $f(y)$ for $x$
2. $\{x/f(z), y/z\}$ — substitutes $z$ for $y$, then $f(z)$ for $x$

Both unifiers work, but which is “better”?

Definition of MGU

A unifier $\sigma$ is most general if for every other unifier $\tau$, there exists a substitution $\rho$ such that:

In other words, $\sigma$ is the “least committed” unifier—it makes the minimal necessary substitutions, leaving maximum flexibility for further instantiation.

Why MGU Matters

1. Completeness: Using MGU ensures we don’t miss solutions by prematurely committing to specific values
2. Efficiency: MGU avoids redundant computation by not computing specialized unifiers
3. Correctness: In proof systems, non-MGU unifiers can introduce spurious constraints that break soundness
4. Reusability: MGU results can be specialized as needed, but specialized results cannot be generalized

Computing the MGU

Unification Algorithm

The standard unification algorithm works recursively:

1. Base case: If terms are identical, return empty substitution
2. Constant-constant: If both constants, succeed only if identical
3. Variable-term: If one is a variable not occurring in the term, substitute
4. Term-term: If both are compound terms (functions), unify recursively and compose

Step-by-Step Examples

Example 1: Simple Variables

Terms: $x$ and $y$

Process:

• $x$ is a variable, $y$ is a variable
• We can set $x \mapsto y$ (or $y \mapsto x$)

MGU: $\{x/y\}$

This is most general because we haven’t committed to any specific value—we just establish that $x$ and $y$ must be equal.

Example 2: Variable and Constant

Terms: $x$ and $a$

Process:

• $x$ is a variable not occurring in constant $a$
• Substitute $a$ for $x$

MGU: $\{x/a\}$

This is the only possible unifier—we must commit to the constant $a$.

Example 3: Compound Terms

Terms: $P(x, f(y))$ and $P(a, f(z))$

Process:

1. Both have predicate $P$ with two arguments—check arguments
2. First arguments: $x$ and $a$ → MGU: $\{x/a\}$
3. Second arguments: $f(y)$ and $f(z)$ → unify $y$ and $z$ → MGU: $\{y/z\}$
4. Compose: $\{x/a, y/z\}$

MGU: $\{x/a, y/z\}$

Example 4: Nested Functions

Terms: $f(g(x), h(y))$ and $f(g(a), h(b))$

Process:

1. Outer function $f$/2: check arguments
2. First argument: $g(x)$ and $g(a)$ → $\{x/a\}$
3. Second argument: $h(y)$ and $h(b)$ → $\{y/b\}$
4. Compose: $\{x/a, y/b\}$

MGU: $\{x/a, y/b\}$

Occurs Check

Critical: We must check if a variable occurs in the term we’re trying to substitute.

Terms: $x$ and $f(x)$

Problem: Substituting $x$ with $f(x)$ creates infinite term $f(f(f(...)))$

Solution: The occurs check detects this and declares unification impossible.

MGU: Does not exist (unification fails)

Practical Examples

In Logic Programming (Prolog)

Prolog uses unification extensively:

% Query: father(john, X) = father(john, bob)
% MGU: {X/bob}

% Query: father(X, Y) = father(john, bob)
% MGU: {X/john, Y/bob}

% Query: loves(X, f(X)) = loves(john, f(john))
% MGU: {X/john}

% Query: loves(X, f(X)) = loves(Y, Y)  
% FAILS - occurs check: X would need to equal f(X)

In Resolution Theorem Proving

Resolution requires unifying complementary literals:

Clause 1:    P(x) ∨ Q(x)
Clause 2:    ¬P(f(y)) ∨ R(y)

To resolve on $P$:

1. Unify $P(x)$ with $P(f(y))$
2. MGU: $\{x/f(y)\}$
3. Apply to both clauses: $Q(f(y)) ∨ R(y)$

In Type Inference

Type inference uses unification to ensure type consistency:

-- Given: map :: (a -> b) -> [a] -> [b]
-- And:   map succ [1,2,3] :: [Int]
-- Unify: a = Int, b = Int
-- MGU: {a/Int, b/Int}

Implementation

Python Implementation of MGU

class Term:
    """Base class for terms."""
    pass

class Var(Term):
    def __init__(self, name):
        self.name = name
    
    def __str__(self):
        return self.name
    
    def __eq__(self, other):
        return isinstance(other, Var) and self.name == other.name

class Const(Term):
    def __init__(self, name):
        self.name = name
    
    def __str__(self):
        return self.name

class Fun(Term):
    def __init__(self, name, args):
        self.name = name
        self.args = args
    
    def __str__(self):
        return f"{self.name}({', '.join(str(a) for a in self.args)})"


def apply_subst(term, subst):
    """Apply substitution to term."""
    if isinstance(term, Var):
        return subst.get(term.name, term)
    elif isinstance(term, Fun):
        return Fun(term.name, [apply_subst(a, subst) for a in term.args])
    return term


def occurs_check(var, term):
    """Check if variable occurs in term."""
    if isinstance(term, Var):
        return var == term
    elif isinstance(term, Fun):
        return any(occurs_check(var, arg) for arg in term.args)
    return False


def unify(t1, t2, subst=None):
    """
    Compute MGU of two terms.
    Returns (success, substitution) tuple.
    """
    if subst is None:
        subst = {}
    
    # Apply current substitution
    t1 = apply_subst(t1, subst)
    t2 = apply_subst(t2, subst)
    
    # Same terms - nothing to do
    if str(t1) == str(t2):
        return True, subst
    
    # Variable-term case
    if isinstance(t1, Var):
        if occurs_check(t1, t2):
            return False, subst  # Occurs check failed
        subst[t1.name] = t2
        return True, subst
    
    if isinstance(t2, Var):
        if occurs_check(t2, t1):
            return False, subst
        subst[t2.name] = t1
        return True, subst
    
    # Function-function case
    if isinstance(t1, Fun) and isinstance(t2, Fun):
        if t1.name != t2.name or len(t1.args) != t2.args):
            return False, subst
        
        for arg1, arg2 in zip(t1.args, t2.args):
            success, subst = unify(arg1, arg2, subst)
            if not success:
                return False, subst
        
        return True, subst
    
    return False, subst


# Example usage
if __name__ == "__main__":
    # P(x, f(y)) and P(a, f(z))
    t1 = Fun("P", [Var("x"), Fun("f", [Var("y")])])
    t2 = Fun("P", [Const("a"), Fun("f", [Var("z")])])
    
    success, mgu = unify(t1, t2)
    print(f"Unification {'succeeded' if success else 'failed'}")
    if success:
        print(f"MGU: {mgu}")
        # Verify: apply_subst(t1, mgu) should equal apply_subst(t2, mgu)

Failure Cases

1. Different Function Symbols

Terms: f(x) and g(x)
MGU: Does not exist

The function symbols $f$ and $g$ are different—no substitution can make these equal.

2. Different Arity

Terms: f(x, y) and f(x)
MGU: Does not exist  

The functions have different numbers of arguments.

3. Occurs Check Failure

Terms: x and f(x)
MGU: Does not exist (would create infinite term)

This is critical for avoiding non-terminating unification.

4. Constant Conflict

Terms: a and b
MGU: Does not exist

Two different constants cannot be unified.

Significance in Automated Reasoning

Resolution Theorem Proving

Resolution relies on finding complementary literals and unifying them. Using MGU ensures:

• Completeness: All resolvable pairs are found
• Correctness: No spurious constraints
• Efficiency: No redundant computation

Logic Programming

In Prolog:

• Query answering uses unification with MGU
• Clause matching requires MGU computation
• The choice of MGU affects which solutions are found first

Type Systems

Modern type inference:

• Hindley-Milner algorithm uses unification
• MGU ensures principal types (most general types)
• Type errors detected through unification failure

Knowledge Representation

Ontologies and description logics:

• Concept unification in classification
• ABox assertions and query answering

Properties of MGU

Existence and Uniqueness

Theorem: If two terms have any unifier, they have a unique MGU (up to variable renaming).

This uniqueness (modulo $\alpha$-conversion) is crucial—it means there’s a canonical representation of the “best” unifier.

Composition

If $\sigma$ is MGU of $s$ and $t$, and $\tau$ is any unifier, then $\tau = \sigma \rho$ for some $\rho$.

Relationship to Anti-Unification

While MGU finds the most general unifier (most specific common instance), anti-unification finds the most general generalization (least specific common ancestor) of two terms.

Conclusion

The Most General Unifier is a foundational concept in automated reasoning. It provides:

1. A canonical way to combine variable instantiations
2. Guaranteed completeness in search procedures
3. Efficient computation through the standard algorithm
4. Theoretical foundation for logic programming and theorem proving

Understanding MGU is essential for anyone working with formal logic, whether building automated provers, writing logic programs, or developing type inference systems. The concept elegantly captures what it means to make terms “as equal as possible” while preserving maximum flexibility for future specialization.

The next time you write a Prolog query or see a type error in your favorite programming language, remember: beneath the surface, the Most General Unifier is hard at work, finding the most general way to make things match.

Further Reading

• Robinson’s 1965 Paper: “A Machine-Oriented Logic Based on the Resolution Principle” — the original unification algorithm
• Algorithm + Data Structures = Logic Programs: Kay/Flatt — Prolog implementation details
• Types and Programming Languages: Benjamin Pierce — type inference and unification
• The Lambda Calculus: Church — related ideas in type theory