mgu

abstract fun mgu(term1: Term, term2: Term, occurCheckEnabled: Boolean = true): Substitution

Calculates the Most General Unifier of term1 and term2, optionally enabling occurs-check.

a Substitution.Unifier (possibly Substitution.empty) binding the variables of term1 and term2 so that applying it to both terms yields syntactically equal results, or Substitution.failed if no such substitution exists (including when occurCheckEnabled is true and unification would otherwise produce a cyclic term, or when context itself is failed).

open fun mgu(term1: Term, term2: Term): Substitution

Calculates the Most General Unifier of term1 and term2, with occurs-check enabled.