Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
From MaRDI portal
Publication:3172889
DOI10.1007/978-3-642-24364-6_11zbMath1348.68219OpenAlexW1872679327MaRDI QIDQ3172889
Publication date: 7 October 2011
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-24364-6_11
Related Items (4)
Size-based termination of higher-order rewriting ⋮ Normal Higher-Order Termination ⋮ Unnamed Item ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proving termination by dependency pairs and inductive theorem proving
- Tyrolean termination tool: techniques and features
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Polymorphic rewriting conserves algebraic strong normalization
- Combinatory reduction systems: Introduction and survey
- Generalized sufficient conditions for modular termination of rewriting
- On the modularity of termination of term rewriting systems
- Abstract data type systems
- Comparing curried and uncurried rewriting
- Termination of term rewriting using dependency pairs
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Automating the dependency pair method
- A Monotonic Higher-Order Semantic Path Ordering
- Simplifying Algebraic Functional Systems
- The Computability Path Ordering: The End of a Quest
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
- Higher Order Dependency Pairs for Algebraic Functional Systems
- Frontiers of Combining Systems
- Uncurrying for Termination
- Term Rewriting and Applications
This page was built for publication: Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
