Solving higher-order equations. From logic to programming
The author claims that it is important to develop techniques for equational reasoning in higher-order logic because due to the expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. The book presents calculi for equational reasoning modulo rewriting rules represented by the higher-order equations. First the general equational reasoning is discussed and next calculi for declarative programming in higher-order logic and \(\lambda\)-calculus are developed. The motivation for that is to achieve integration and generalization of declarative programming paradigms in higher-order logic. The higher-order narrowing is used as an inference rule generalizing the inference mechanisms in both logic and functional programming. In particular, the reader can find in the book some decidable second-order unification problems, narrowing calculi suitable in the higher-order case, several refinements of lazy narrowing for general equational reasoning, a new approach to higher-order functional-logic programming based on narrowing as well as some examples like the simple parser or the alternating bit protocol showing the utility of having both paradigms, functional and logic programming in one setting.
- Logic programming with equations
- Combining Logic Programming and Equation Solving
- scientific article; zbMATH DE number 1552533
- scientific article; zbMATH DE number 4164143
- scientific article; zbMATH DE number 3958699
- scientific article; zbMATH DE number 4047723
- An equational approach to logic programming
- scientific article; zbMATH DE number 3988745
- Higher-dimensional word problems with applications to equational logic
- An algorithm for the solution of systems of logical equations
- A decision algorithm for distributive unification
- Developing developments
- HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
- scientific article; zbMATH DE number 2086320 (Why is no real title available?)
- Cooperation of algebraic constraint domains in higher-order functional and logic programming
- scientific article; zbMATH DE number 2000434 (Why is no real title available?)
- Higher-order equational logic for specification, simulation and testing
- Development closed critical pairs
- Efficient full higher-order unification
- Higher-order narrowing with convergent systems
- How to prove decidability of equational theories with second-order computation analyser SOL
- A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains
- Inductive-data-type systems
- The Clausal Theory of Types
- Nominal equational narrowing: rewriting for unification in languages with binders
This page was built for publication: Solving higher-order equations. From logic to programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4229811)
