Unification types in logic

the long version

The main aim of unification is to make two symbolic expressions equal, or identical, by substituting their variables with other expressions. Unification in logic is concerned with finding a substitution that transforms a formula into a theorem or a tautology. The substitutions that satisfy this condition are called unifiers. The crucial problem considered in the unification theory is to find, if possible, most general unifiers, i.e., such unifiers for which any unifier is their special case, or instance. There are four possible unification types: unitary (best), finitary, infinitary and nullary, depending on the number of unifiers which are maximal with respect to the relation of being more general. The subject of this book is to assign these types to various logical systems, to find the properties determining particular types of logics together with their location, and to apply unifiers to logic. In general our investigations concern the logical analysis of language and its structure.