Harnessing first order termination provers using higher order dependency pairs
From MaRDI portal
(Redirected from Publication:3172889)
Recommendations
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)
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)
