Instantiation theory. On the foundations of automated deduction (Q1202066)

Instantiation, or the theory of variable substitution in terms, is studied here in an abstract setting. In order to make the theory as general and clean as possible, the basic concepts are introduced axiomatically, so that, rather than working upon any particular formalism, such as the terms of first-order predicate logic or lambda- calculus, all such term systems are examples. The climax of the text is a unification algorithm which is proven to be sound and, under appropriate conditions, complete; the complexity of the algorithm is also discussed. Other topics along the way include further properties that an instantiation system might enjoy, such as various degrees of type strictness and well-foundedness of terms, and quotient system, subsystems, and homomorphisms.