Unification Theory

著者: Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauß, Klaus U. Schulz - Elsevier eBooks 1999 被引用: 218

Unification is a fundamental process upon which many methods for automated de­duction 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 intro­ductory section, we will 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.