Decreasing diagrams and relative termination
From MaRDI portal
Publication:438562
DOI10.1007/s10817-011-9238-xzbMath1243.68199OpenAlexW1997678912MaRDI QIDQ438562
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9238-x
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
A proof method for local sufficient completeness of term rewriting systems ⋮ Relative termination via dependency pairs ⋮ Unnamed Item ⋮ CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Regular Patterns in Second-Order Unification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ De Bruijn's weak diamond property revisited ⋮ Confluence by critical pair analysis revisited ⋮ Composing proof terms ⋮ Labelings for decreasing diagrams
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- KBO orientability
- Matrix interpretations for proving termination of term rewriting
- Higher-order rewrite systems and their confluence
- Confluence by decreasing diagrams
- Developing developments
- Isabelle/HOL. A proof assistant for higher-order logic
- Modular properties of composable term rewriting systems
- Combinatory logic. Vol. II
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Confluence by Decreasing Diagrams
- Solving Partial Order Constraints for LPO Termination
- Generalizing Newman’s Lemma for Left-Linear Rewrite Systems
- Proving Confluence of Term Rewriting Systems Automatically
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
- Labelings for Decreasing Diagrams.
- Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling.
- Modular Complexity Analysis via Relative Complexity
- Tree-Manipulating Systems and Church-Rosser Theorems
- Decreasing Diagrams and Relative Termination
This page was built for publication: Decreasing diagrams and relative termination
