First-order unification and matching algorithms.

This crate provides algorithms for finding substitutions that make terms equal:

• [unify] - Most general unifier (MGU) of two terms
• [match_term] - One-way matching: find a substitution making a pattern equal to a target

Multiple algorithm implementations are available for educational comparison:

• [robinson] - Classic recursive algorithm (simple, easy to understand)

Examples

use mrs_core::{Term, SymbolTable};
use mrs_unify::unify;

let mut syms = SymbolTable::new();
let f = syms.intern("f");
let a = syms.intern("a");

// Unify f(X, a) with f(b, Y)
let b = syms.intern("b");
let t1 = Term::app(f, vec![Term::var(0), Term::constant(a)]);
let t2 = Term::app(f, vec![Term::constant(b), Term::var(1)]);

let mgu = unify(&t1, &t2).unwrap();
// X -> b, Y -> a
assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(b));
assert_eq!(mgu.apply_term(&Term::var(1)), Term::constant(a));