Instantiation theory is introduced and discussed. The theory aims at giving an abstract framework for instantiation that is applicable to various logic formalisms. The book focuses on the algebraic properties of instantiation, and it is intended as a contribution to a foundation for a general deduction theory. A general theory of instantiation is proposed as the starting point to determine the applicability of what is known about instantiation in specific formal systems.

The book is organized in ten sections, an appendix, and the bibliography. After a general introduction to the book and its organization in section 1, basic facts about monoid actions are reviewed, and the unification problem is introduced in its most general form, with several examples (section 2). A theory of instantiation systems is then introduced, and related approaches to instantiation are recalled, in section 3. In section 4, the author identifies properties that lead to a classification of these systems, and that give a basis for discussing fixed points of substitutions. In section 5, the concept of quotient homomorphism is discussed. Section 6 is devoted to the axiomatic description of construct bases, and it analyzes properties of terms and constructs that permit the construction of efficient unification algorithms. Next, sections 7, 8, and 9 are aimed at producing a generally applicable algorithm that is sound, complete, and efficient. In particular, Williams attempts to correlate soundness and completeness for unification in abstract instantiation systems with analogous requirements in concrete term implementations in sections 8 and 9. Section 10 gives some hints on related issues that are not discussed in the book. The appendix gives the results of the implementation of a general unification algorithm whose construction is an application of the theory.

The book is intended for a specialized mathematical audience. It is an interesting attempt to offer a unifying view of problems connected to instantiation, which are usually found within specific theories. The numerous concepts and notions are introduced in a formal way; notwithstanding the brief informal explanations at the beginning of sections, the book is difficult to read.