A Proof Theory for General Unification

✍ Scribed by Wayne Snyder

• Publisher: Springer
• Year: 1991
• Tongue: English
• Leaves: 188
• Series: Progress in Computer Science and Applied Logic 11
• Edition: 1
• Category: Library

✦ Table of Contents

Cover......Page 1
Editor......Page 2
Title: A Proof Theoryfor General Unification......Page 3
511.3--dc20......Page 4
Table of Contents......Page 6
Preface......Page 8
CHAPTER 1: INTRODUCTION......Page 10
CHAPTER 2: PREVIEW......Page 16
3.1 Algebraic Background......Page 26
3.2 Substitutions......Page 29
3.3 Unification by Transformations on Systems......Page 32
3.4 Equational Logic......Page 37
3.5 Term Rewriting......Page 42
3.5.1 Termination Orderings......Page 43
3.5.2 Confiuence......Page 46
3.6 Completion of Equational Theories......Page 53
4.1 Basic Definitions and Results......Page 58
4.2 Methods for E-Unification......Page 61
5.1 The Set of Transformations BT......Page 70
5.2 Soundness of the Set BT......Page 74
5.3 Completeness of the Set BT......Page 76
6.1 Ground Church-Rosser Systems......Page 92
6.2 Completeness of the Set T......Page 102
6.3 Surreductioll......Page 113
6.4 Completeness of T Revisited......Page 118
6.5 Relaxed Paramodulatioll......Page 121
6.6 Previous Work......Page 126
6.7 Eager Variable Elimination......Page 128
6.8 Current and Future Work......Page 129
6.9 Conclusion......Page 131
7.1 Preliminaries......Page 132
7.2 Higher Order Unification via Transformations......Page 142
7.2.1 Transformations for Higher Order Unification......Page 145
7.2.2 Soundness of the 'Iransformations......Page 152
7.2.3 Completeness of the Transformations......Page 153
7.3 Huet's Procedure Revisited......Page 158
7.4 Conclusion......Page 161
CHAPTER 8: CONCLUSION......Page 163
Appendix 1: DET~RMINISTIC E-UNIFICATION......Page 166
Appendix 2: HUET'S UNIFICATION PROCEDURE......Page 170
Appendix 3: HERBRAND'S UNIFICATION ALGORITHM......Page 174
BIBLIOGRAPHY......Page 176
List of Publications......Page 186
Back Cover......Page 188