Unification

Unification is an algorithm for comparing terms with holes (called unification variables) for equality, discovering substitutions for the unification variables which make those terms equal. Unification of LF terms is used in a variety of ways in STELF:

• During type and term reconstruction, unification is used to infer omitted type and term information.
• In the logic programming operational semantics of LF, unification is used to find solutions to unification variables in queries.

Unification for LF terms requires higher-order unification, which is undecidable. However, many instances of unification that arise in STELF fall into the pattern fragment, which is decidable. Those that are not in the pattern fragment are postponed as constraints; unresolved constraints are reported to the user.