Harnessing first order termination provers using higher order dependency pairs

DOI10.1007/978-3-642-24364-6_11zbMATH Open1348.68219OpenAlexW1872679327MaRDI QIDQ3172889FDOQ3172889

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

Recommendations

• Frontiers of Combining Systems
• A termination ordering for higher order rewrite systems
• Automated Reasoning
• Termination of term rewriting using dependency pairs
• Higher order dependency pairs for algebraic functional systems

zbMATH Keywords

modularityterminationdependency pairshigher-order rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Combinatory reduction systems: Introduction and survey
• Termination of term rewriting using dependency pairs
• Title not available (Why is that?)
• Comparing curried and uncurried rewriting
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Automating the dependency pair method
• Higher Order Dependency Pairs for Algebraic Functional Systems
• Frontiers of Combining Systems
• Uncurrying for Termination
• Term Rewriting and Applications
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Proving termination by dependency pairs and inductive theorem proving
• Title not available (Why is that?)
• Generalized sufficient conditions for modular termination of rewriting
• On the modularity of termination of term rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Polymorphic rewriting conserves algebraic strong normalization
• Abstract data type systems
• The Computability Path Ordering: The End of a Quest
• SAT solving for termination proofs with recursive path orders and dependency pairs
• A Monotonic Higher-Order Semantic Path Ordering
• Simplifying Algebraic Functional Systems
• Argument filterings and usable rules for simply typed dependency pairs

Cited In (6)

• Strongly first order, domain independent dependencies: the union-closed case
• Size-based termination of higher-order rewriting
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• Normal Higher-Order Termination
• Automated Reasoning
• Title not available (Why is that?)

Uses Software

• Haskell
• Tyrolean
• AProVE

This page was built for publication: Harnessing first order termination provers using higher order dependency pairs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172889)