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.