Unification theory. (English) Zbl 1011.68126

Baader, Franz; Snyder, Wayne

Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier; 0-444-50812-0 (vol. 2); 0-444-50813-9 (set)). 445-533 (2001).

Introduction: Unification is a fundamental process upon which many methods for automated deduction are based. Unification theory abstracts from the specific applications of this process: it provides formal definitions for important notions like instantiation, most general unifier, etc., investigates properties of these notions, and provides and analyzes unification algorithms that can be used in different contexts. In this introductory section, we first present the concept of unification in an informal way, then make some historical remarks on where unification was originally introduced, and finally explain our approach to writing this chapter.
For the entire collection see [Zbl 0964.00020].

MSC:

68T15

Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

unification; automated deduction