unicode_fol_kit.unify¶
- unicode_fol_kit.unify(t1, t2, subst=None)[source]¶
Most-general unifier of t1 and t2, or None if they do not unify.
Robinson’s algorithm with occurs-check. The result is a dict mapping variable NAME -> term such that applying it to t1 and t2 (via apply_subst) yields structurally equal nodes. An empty dict means the terms are already equal / trivially unifiable.
Accepts Variable, Constant, Number, Function term nodes, or two Atoms (which unify iff they share predicate and arity and their arguments unify pairwise). The optional subst argument is treated as immutable: it is copied before extension, never modified in place.