NAME
Logic::Relational::Unifier - Performs structural unification of logic terms.
SYNOPSIS
use Logic::Relational::Unifier qw(unify);
my $new_subst = unify($term1, $term2, $subst);
DESCRIPTION
Logic::Relational::Unifier provides structural unification. It implements the standard unification algorithm with an occurs check to prevent infinite terms.
FUNCTIONS
unify
Performs unification of two terms under a given Logic::Relational::Substitution. Returns the updated substitution if unification succeeds, or undef if it fails. Raises an exception if the occurs check fails.
bind_variable
Binds a variable to a term, checking that the variable does not occur inside the term (occurs check).
occurs_in
Helper function. Returns true if the variable ID occurs inside the dereferenced term.