Proving Confluence of Term Rewriting Systems Automatically
From MaRDI portal
Recommendations
- Ground confluence prover based on rewriting induction
- Term Rewriting and Applications
- Proving confluence of term rewriting systems via persistency and decreasing diagrams
- Disproving confluence of term rewriting systems by interpretation and ordering
- Confluence of non-left-linear TRSs via relative termination
Cites work
- A new parallel closed condition for Church-Rosser of left-linear term rewriting systems
- Computer Science Logic
- Confluence by decreasing diagrams
- Confluence by Decreasing Diagrams
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Developing developments
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 4106267 (Why is no real title available?)
- scientific article; zbMATH DE number 1088026 (Why is no real title available?)
- scientific article; zbMATH DE number 1543072 (Why is no real title available?)
- scientific article; zbMATH DE number 794237 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Mechanizing and improving dependency pairs
- Modular properties of composable term rewriting systems
- On the Church-Rosser property for the direct sum of term rewriting systems
- Proving Confluence of Term Rewriting Systems Automatically
- Term Rewriting and All That
- Term Rewriting and Applications
- Termination of term rewriting: Interpretation and type elimination
- Tree-Manipulating Systems and Church-Rosser Theorems
Cited in
(29)- Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems
- Certifying proofs in the first-order theory of rewriting
- Ground confluence of order-sorted conditional specifications modulo axioms
- Conditions for confluence of innermost terminating term rewriting systems
- Labelings for decreasing diagrams
- Confluence of orthogonal term rewriting systems in the prototype verification system
- CSI: new evidence -- a progress report
- Nominal confluence tool
- Certification of classical confluence results for left-linear term rewrite systems
- Disproving confluence of term rewriting systems by interpretation and ordering
- Certifying confluence proofs via relative termination and rule labeling
- CoLL: a confluence tool for left-linear term rewrite systems
- Proving Confluence of Term Rewriting Systems Automatically
- Decreasing diagrams and relative termination
- Improving rewriting induction approach for proving ground confluence
- CSI -- a confluence tool
- Certifying confluence of almost orthogonal CTRSs via exact tree automata completion
- Ground confluence prover based on rewriting induction
- scientific article; zbMATH DE number 6792369 (Why is no real title available?)
- Decreasing diagrams and relative termination
- An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
- Compositional confluence criteria
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
- Proving confluence in the confluence framework with confident
- A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems
- Sort-based confluence criteria for non-left-linear higher-order rewriting
- Confluence of logically constrained rewrite systems revisited
This page was built for publication: Proving Confluence of Term Rewriting Systems Automatically
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3636821)
