Author | Snyder, Wayne. author |
---|---|
Title | A Proof Theory for General Unification [electronic resource] / by Wayne Snyder |
Imprint | Boston, MA : Birkhรคuser Boston : Imprint: Birkhรคuser, 1991 |
Connect to | http://dx.doi.org/10.1007/978-1-4612-0435-0 |
Descript | VII, 178 p. online resource |
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