Module unification 

First-Order Unification

This module implements Robinson’s unification algorithm for first-order terms. Unification is a fundamental operation in automated theorem proving, logic programming, and type inference.

Overview

Unification finds a most general unifier (MGU) that makes two terms syntactically equal:

• Given terms s and t, find substitution θ such that sθ = tθ
• The MGU is the most general such substitution (no more specific than necessary)

Examples

use tensorlogic_ir::{Term, Substitution, unify_terms};

// Unify P(x, f(y)) with P(a, f(b))
let term1 = Term::var("x");
let term2 = Term::constant("a");

let result = unify_terms(&term1, &term2);
assert!(result.is_ok());
let subst = result.unwrap();
assert_eq!(subst.apply(&term1), term2);

Algorithm

We use Robinson’s unification algorithm with occur-check:

1. If both terms are identical, return empty substitution
2. If one is a variable, bind it to the other (with occur-check)
3. If both are compound terms, recursively unify arguments
4. Otherwise, unification fails

Applications

• Theorem Proving: Resolution requires unification of complementary literals
• Logic Programming: Pattern matching in Prolog-style languages
• Type Inference: Hindley-Milner type inference uses unification
• Sequent Calculus: Term substitution in quantifier rules

Structs

Substitution

A substitution maps variables to terms.

Functions

anti_unify_terms

Anti-unification finds the most specific generalization (MSG) of two terms.

are_unifiable

Check if two terms are unifiable (without computing the unifier).

lgg_terms

Compute the least general generalization (LGG) of a list of terms.

rename_vars

Rename variables in a term to avoid conflicts.

unify_term_list

Attempt to unify a list of term pairs.

unify_terms

Unify two terms, returning the most general unifier (MGU).