A Proof Theory for General Unification
In this monograph we study two generalizations of standard unification, E-unification and higher-order unification, using an abstract approach orig inated by Herbrand and developed in the case of standard first-order unifi cation by Martelli and Montanari. The formalism presents the unification co...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Boston, MA
Birkhäuser
1991, 1991
|
| Edition: | 1st ed. 1991 |
| Series: | Progress in Computer Science and Applied Logic
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 1: Introduction
- 2: Preview
- 3: Preliminaries
- 3.1 Algebraic Background
- 3.2 Substitutions
- 3.3 Unification by Transformations on Systems
- 3.4 Equational Logic
- 3.5 Term Rewriting
- 3.6 Completion of Equational Theories
- 4: E-Unification
- 4.1 Basic Definitions and Results
- 4.2 Methods for E-Unification
- 5: E-Unification via Transformations
- 5.1 The Set of Transformations BT
- 5.2 Soundness of the Set BT
- 5.3 Completeness of the Set BT
- 6: An Improved Set of Transformations
- 6.1 Ground Church-Rosser Systems
- 6.2 Completeness of the Set T
- 6.3 Surreduction
- 6.4 Completeness of the Set T Revisited
- 6.5 Relaxed Paramodulation
- 6.6 Previous Work
- 6.7 Eager Variable Elimination
- 6.8 Current and Future Work
- 6.9 Conclusion
- 7: Higher Order Unification
- 7.1 Preliminaries
- 7.2 Higher Order Unification via Transformations
- 7.3 Huet’s Procedure Revisited
- 7.4 Conclusion
- 8: Conclusion
- Appendices