Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

DOI10.1007/978-3-642-24364-6_11zbMath1348.68219OpenAlexW1872679327MaRDI QIDQ3172889

Carsten Fuhs, Cynthia Kop

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

zbMATH Keywords

terminationmodularityhigher-order rewritingdependency pairs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

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

• Haskell
• Tyrolean
• AProVE

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