Function unify_terms 

pub fn unify_terms(t1: &ProofTerm, t2: &ProofTerm) -> ProofResult<Substitution>

Unify two terms, returning the Most General Unifier (MGU).

The MGU is the smallest substitution that makes both terms identical. Uses Robinson’s algorithm with occurs check.

Arguments

• t1 - The first term (often a pattern with variables)
• t2 - The second term (often a ground term or another pattern)

Returns

• Ok(subst) - A substitution that unifies the terms
• Err(OccursCheck) - If unification would create an infinite term
• Err(SymbolMismatch) - If function/constant names differ
• Err(ArityMismatch) - If argument counts differ

Example

use logicaffeine_proof::{ProofTerm, unify::unify_terms};

let pattern = ProofTerm::Function(
    "Mortal".into(),
    vec![ProofTerm::Variable("x".into())]
);
let target = ProofTerm::Function(
    "Mortal".into(),
    vec![ProofTerm::Constant("Socrates".into())]
);

let subst = unify_terms(&pattern, &target).unwrap();
assert_eq!(
    subst.get("x"),
    Some(&ProofTerm::Constant("Socrates".into()))
);

See Also

• unify_exprs - Unifies expressions (handles quantifiers, connectives)
• apply_subst_to_term - Applies the resulting substitution