Unification in logic

Abstract

There are many problems in mathematics that can be cast in terms of unification, meaning that a solution of the problem is a substitution that identifies two terms, either literally, or against a background theory of equivalence. In the context of logics, a unifier is a substitution under which a formula becomes derivable in the logic. In classical propositional logic, all unifiable formulas have a most general unifier, which is a unifier that generates all other unifiers of a formula. Nonclassical logics in general do not have this useful property, but many modal and intermediate propositional logics satisfy a slightly weaker property. In these logics, for every formula there is a finite set of unifiers such that any other unifier of the formula is generated by one of them.