This monograph develops techniques for equational reasoning in higher-order logic. Due to its expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. In these applica tions, higher-order logic provides the necessary level of abstraction for con cise and natural formulations. The main assets of higher-order logic are quan tification over functions or predicates and its abstraction mechanism. These allow one to represent quantification in formulas and other variable-binding constructs. In this book, we focus on equational logic as a fundamental and natural concept in computer science and mathematics. We present calculi for equa tional reasoning modulo higher-order equations presented as rewrite rules. This is followed by a systematic development from general equational rea soning towards effective calculi for declarative programming in higher-order logic and A-calculus. This aims at integrating and generalizing declarative programming models such as functional and logic programming. In these two prominent declarative computation models we can view a program as a logical theory and a computation as a deduction.
Inhaltsverzeichnis
1 Introduction. - 2 Preview. - 2. 1 Term Rewriting. - 2. 2 Narrowing. - 2. 3 Narrowing and Logic Programming. - 2. 4 ? -Calculus and Higher-Order Logic. - 2. 5 Higher-Order Term Rewriting. - 2. 6 Higher-Order Unification. - 2. 7 Decidability of Higher-Order Unification. - 2. 8 Narrowing: The Higher-Order Case. - 3 Preliminaries. - 3. 1 Abstract Reductions and Termination Orderings. - 3. 2 Higher-Order Types and Terms. - 3. 3 Positions in ? -Terms. - 3. 4 Substitutions. - 3. 5 Unification Theory. - 3. 6 Higher-Order Patterns. - 4 Higher-Order Equational Reasoning. - 4. 1 Higher-Order Unification by Transformation. - 4. 2 Unification of Higher-Order Patterns. - 4. 3 Higher-Order Term Rewriting. - 5 Decidability of Higher-Order Unification. - 5. 1 Elimination Problems. - 5. 2 Unification of Second-Order with Linear Terms. - 5. 3 Relaxing the Linearity Restrictions. - 5. 4 Applications and Open Problems. - 6 Higher-Order Lazy Narrowing. - 6. 1 Lazy Narrowing. - 6. 2 Lazy Narrowing with Terminating Rules. - 6. 3 Lazy Narrowing with Left-Linear Rules. - 6. 4 Narrowing with Normal Conditional Rules. - 6. 5 Scope and Completeness of Narrowing. - 7 Variations of Higher-Order Narrowing. - 7. 1 A General Notion of Higher-Order Narrowing. - 7. 2 Narrowing on Patterns with Pattern Rules. - 7. 3 Narrowing Beyond Patterns. - 7. 4 Narrowing on Patterns with Constraints. - 8 Applications of Higher-Order Narrowing. - 8. 1 Functional-Logic Programming. - 8. 2 Equational Reasoning by Narrowing. - 9 Concluding Remarks. - 9. 1 Related Work. - 9. 2 Further Work.
