Harnessing first order termination provers using higher order dependency pairs

DOI10.1007/978-3-642-24364-6_11MaRDI QIDQ3172889zbMATH OpenOpenAlexFDO

Authors 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

modularityterminationdependency pairshigher-order rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

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

Cites work

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

Cited in

(8)

• Normal higher-order termination
• 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
• Automated Reasoning
• Wanda -- a higher-order termination tool (system description)
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)

Describes a project that uses

Uses Software

• AProVE
• Tyrolean
• Haskell

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)