pith. sign in

arxiv: 2306.16330 · v3 · submitted 2023-06-28 · 💻 cs.LO · cs.PL

Proving Confluence in the Confluence Framework with CONFident

Ra\'ul Guti\'errez , Salvador Lucas , Miguel V\'itores This is my paper

Pith reviewed 2026-05-24 08:19 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords confluenceterm rewriting systemsgeneralized term rewritingconditional rulesmodular proof strategiescontext-sensitive rewritingautomated confluence analysis
0
0 comments X

The pith

The Confluence Framework uses a divide-and-conquer strategy to automatically prove and disprove confluence of generalized term rewriting systems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents the Confluence Framework as a way to organize multiple confluence techniques into a single proof tree. It targets Generalized Term Rewriting Systems, which permit rewriting only at selected arguments of symbols and support a broad class of conditional rules. These systems include context-sensitive term rewriting, string rewriting, and conditional rewriting as special cases. A reader would care because the approach automates analysis that previously required manual effort or was limited to simpler systems. The implementation shows the strategy can both establish confluence and find counterexamples for disproof.

Core claim

The Confluence Framework organizes techniques such as modular decompositions, joinability checks on conditional critical and variable pairs, and transformations into proof trees through a divide-and-conquer modular strategy. This handles Generalized Term Rewriting Systems where rewriting occurs only in chosen arguments and conditional rules are allowed, thereby covering several standard variants of term rewriting systems as particular cases.

What carries the argument

The divide-and-conquer modular strategy that assembles confluence techniques and auxiliary tasks such as joinability checks into a single proof tree.

If this is right

  • Confluence proofs become possible for context-sensitive term rewriting systems, string rewriting systems, and conditional term rewriting systems as direct instances.
  • Both positive proofs of confluence and explicit disproofs via non-joinable pairs can be generated automatically.
  • Techniques including transformations and modular decompositions can be applied together without separate manual coordination.
  • Auxiliary tasks such as checking joinability of conditional pairs are integrated directly into the overall proof procedure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same divide-and-conquer structure could be reused to automate other properties such as termination or reachability for the same class of systems.
  • Extending the framework to handle higher-order or infinite-state rewriting would require only new leaf techniques while keeping the tree structure.
  • Integration into existing rewriting engines could allow confluence checks during program transformation or compiler optimization pipelines.

Load-bearing premise

The modular strategy combines different confluence techniques in a proof tree without introducing unsoundness.

What would settle it

A concrete generalized term rewriting system for which the implementation returns a confluence verdict that disagrees with an independent manual proof or counterexample.

Figures

Figures reproduced from arXiv: 2306.16330 by Miguel V\'itores, Ra\'ul Guti\'errez, Salvador Lucas.

Figure 1
Figure 1. Figure 1: Sentences for different semantics of CS-CTRSs [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Non-joinability as infeasibility in Example 5.37 [PITH_FULL_IMAGE:figures/full_fig_p030_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Proof trees for confluence problems of CTRSs and CS- [PITH_FULL_IMAGE:figures/full_fig_p031_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Proof trees for confluence problems of CTRSs and TRS [PITH_FULL_IMAGE:figures/full_fig_p031_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Proof strategy for (CS-)TRSs Confluence no PEVar PInl PSimp PUconf POrth yes PKB ∅ 6= ∅ yes PWCR Local Confluence no PEVar PInl PSimp PCR PHE 6= ∅ ∅ yes Joinability PJO yes no [PITH_FULL_IMAGE:figures/full_fig_p033_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Proof strategy for (CS-)CTRSs [PITH_FULL_IMAGE:figures/full_fig_p033_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The CS-CTRS R⊥ in Example 1.1 in COPS (left) and TPDB (right) format 7.1. Input format The main input format to introduce rewrite systems in CONFident is the COPS format,7 the offi￾cial input format of the Confluence Competition (CoCo8 ). The (older) TPDB format9 can also be used. As an example, [PITH_FULL_IMAGE:figures/full_fig_p034_7.png] view at source ↗
read the original abstract

This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically prove and disprove confluence of *Generalized Term Rewriting Systems*, where (i) only selected arguments of function symbols can be rewritten and (ii) a rather general class of conditional rules can be used. This includes, as particular cases, several variants of rewrite systems such as (context-sensitive) *term rewriting systems*, *string rewriting systems*, and (context-sensitive) *conditional term rewriting systems*. The divide-and-conquer modular strategy allows us to combine in a proof tree different techniques for proving confluence, including modular decompositions, checking joinability of (conditional) critical and variable pairs, transformations, etc., and auxiliary tasks required by them, e.g., joinability of terms, joinability of conditional pairs, etc.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The manuscript introduces the Confluence Framework, a divide-and-conquer modular strategy for automatically proving and disproving confluence of Generalized Term Rewriting Systems (GTRSs). GTRSs generalize context-sensitive TRSs, string rewriting systems, and conditional TRSs by allowing selected arguments to be rewritten and using a broad class of conditional rules. The framework is implemented in the CONFident tool and combines techniques including modular decompositions, joinability checks on conditional critical/variable pairs, and transformations inside a proof tree, along with auxiliary tasks such as term joinability.

Significance. If the modular combination rules are shown to be sound, the result would meaningfully extend the scope of automated confluence analysis beyond standard TRSs. The implementation in CONFident and the ability to both prove and disprove confluence for the generalized class constitute a practical contribution. The paper's emphasis on a unified proof-tree construction for disparate techniques is a clear strength.

major comments (2)
  1. [§3.2] §3.2 (Proof-tree construction): The rules for combining subproblems arising from conditional critical pairs and variable pairs do not explicitly address preservation of joinability when conditions involve extra variables or when context-sensitivity restricts rewriting positions; this combination step is load-bearing for the central claim that the framework remains sound for the full class of GTRSs.
  2. [§4.1] §4.1 (Soundness theorem): The statement that the modular strategy inherits soundness from the individual techniques assumes subproblem independence, but the argument does not contain an explicit lemma showing that context-sensitivity annotations and conditional guards do not introduce new critical pairs that violate the independence assumption.
minor comments (3)
  1. Notation for conditional pairs is introduced without a dedicated definition table; a small table listing the different pair kinds and their joinability predicates would improve readability.
  2. Figure 2 (example proof tree) uses abbreviations for technique names that are only expanded in the caption; inline expansion on first use would help readers follow the modular decomposition.
  3. The experimental section reports success rates on a benchmark but does not list the precise timeout or memory limits used by CONFident; these parameters should be stated explicitly.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address the two major comments point by point below, indicating where we agree that additional clarification or a new lemma is warranted.

read point-by-point responses

  1. Referee: [§3.2] §3.2 (Proof-tree construction): The rules for combining subproblems arising from conditional critical pairs and variable pairs do not explicitly address preservation of joinability when conditions involve extra variables or when context-sensitivity restricts rewriting positions; this combination step is load-bearing for the central claim that the framework remains sound for the full class of GTRSs.

    Authors: We agree that the interaction between extra variables in conditions and context-sensitivity restrictions merits an explicit remark. In the framework, extra variables are instantiated as fresh constants during joinability checks, and context-sensitivity is already encoded in the definition of the critical-pair and variable-pair generation steps; the combination rules therefore inherit joinability preservation from these definitions. Nevertheless, to make the argument fully transparent we will insert a short clarifying paragraph immediately after the combination rules in §3.2. This constitutes a partial revision focused on exposition rather than a change to the rules themselves. revision: partial

  2. Referee: [§4.1] §4.1 (Soundness theorem): The statement that the modular strategy inherits soundness from the individual techniques assumes subproblem independence, but the argument does not contain an explicit lemma showing that context-sensitivity annotations and conditional guards do not introduce new critical pairs that violate the independence assumption.

    Authors: The referee is correct that an explicit supporting lemma would strengthen the presentation. While the independence of subproblems follows from the fact that both context-sensitivity annotations and conditional guards are folded into the generation of critical pairs (so that no additional pairs arise outside those already considered), we did not isolate this fact as a separate lemma. We will add a short lemma in §4.1 that states and proves the required independence property for GTRSs. This will be a full revision. revision: yes

Circularity Check

0 steps flagged

No circularity: novel framework construction with independent soundness claims

full rationale

The paper presents the Confluence Framework as a new divide-and-conquer modular strategy for combining confluence techniques (modular decompositions, joinability checks, transformations) in proof trees for generalized TRSs. No equations, fitted parameters, or self-referential definitions appear in the abstract or description. The central construction is described as a novel combination rather than a renaming or reduction of prior results by construction. Individual techniques are treated as independently established, and the modular soundness is positioned as an assumption of the framework rather than derived from self-citation chains or ansatzes within the paper. This is a standard self-contained presentation of a proof tool.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central contribution is the new framework itself; it relies on standard domain assumptions from term rewriting theory but introduces the modular strategy as the novel element.

axioms (1)
  • domain assumption Standard properties of confluence and critical pairs extend to the generalized term rewriting systems described.
    The framework builds directly on existing theory of term rewriting without re-deriving these properties.
invented entities (1)
  • Confluence Framework no independent evidence
    purpose: Modular divide-and-conquer strategy for confluence proofs in generalized systems.
    This is the primary new contribution introduced by the paper.

pith-pipeline@v0.9.0 · 5697 in / 1320 out tokens · 48945 ms · 2026-05-24T08:19:56.310440+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

80 extracted references · 80 canonical work pages

  1. [1]

    Local confluence of conditional and generalized term rewriting systems

    Lucas S. Local confluence of conditional and generalized term rewriting systems. Journal of Logical and Algebraic Methods in Programming , 2024. 136:paper 100926, pages 1–23. doi:10.1016/j.jlamp.2023. 100926

    work page doi:10.1016/j.jlamp.2023 2024

  2. [2]

    Context-sensitive Rewriting

    Lucas S. Context-sensitive Rewriting. ACM Comput. Surv. , 2020. 53(4):78:1–78:36. doi:10.1145/ 3397677

    work page 2020

  3. [3]

    Term Rewriting and All That

    Baader F, Nipkow T. Term Rewriting and All That. Cambridg e University Press, 1998. ISBN 978-0-521- 45520-6. doi:10.1017/CBO9781139172752

    work page doi:10.1017/cbo9781139172752 1998

  4. [4]

    The (generaliz ed) Post correspondence problem with lists consisting of two words is decidable

    Kaplan S. Conditional Rewrite Rules. Theor . Comput. Sci. , 1984. 33:175–193. doi:10.1016/0304- 3975(84)90087-2

    work page doi:10.1016/0304- 1984

  5. [5]

    Applications and extensions of context-sensit ive rewriting

    Lucas S. Applications and extensions of context-sensit ive rewriting. Journal of Logical and Algebraic Methods in Programming, 2021. 121:100680. doi:10.1016/j.jlamp.2021.100680

    work page doi:10.1016/j.jlamp.2021.100680 2021

  6. [6]

    Transformational Approaches for Condition al Term Rewrite Systems

    Gmeiner KS. Transformational Approaches for Condition al Term Rewrite Systems. Ph.D. thesis, Faculty of Informatics, Vienna University of Technology, 2014

    work page 2014

  7. [7]

    Advanced Topics in Term Rewriting

    Ohlebusch E. Advanced Topics in Term Rewriting. Springe r, 2002. ISBN 978-0-387-95250-5. doi: 10.1007/978-1-4757-3661-8

    work page doi:10.1007/978-1-4757-3661-8 2002

  8. [8]

    The Dependency Pa ir Framework: Combining Techniques for Automated Termination Proofs

    Giesl J, Thiemann R, Schneider-Kamp P . The Dependency Pa ir Framework: Combining Techniques for Automated Termination Proofs. In: Baader F, V oronkov A (eds .), Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conferen ce, LP AR 2004, Proceedings, volume 3452 of Lecture Notes in Computer Science . Springer, 2004 pp. 301–33...

    work page doi:10.1007/978-3-540-3227 2004

  9. [9]

    Mechaniz ing and Improving Dependency Pairs

    Giesl J, Thiemann R, Schneider-Kamp P , Falke S. Mechaniz ing and Improving Dependency Pairs. J. Autom. Reasoning, 2006. 37(3):155–203. doi:10.1007/s10817-006-9057-7

    work page doi:10.1007/s10817-006-9057-7 2006

  10. [10]

    Dependency Pairs Ter mination in Dependent Type Theory Modulo Rewriting

    Blanqui F, Genestier G, Hermant O. Dependency Pairs Ter mination in Dependent Type Theory Modulo Rewriting. In: Geuvers H (ed.), 4th International Conferen ce on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of Leibniz International Proceedings in Informatics (LIPIcs) . Schloss Dagstuhl - Leibn...

    work page doi:10.4230/lipics.fscd.2019.9 2019

  11. [11]

    Dependency Pairs for Rewriting with No n-free Constructors

    Falke S, Kapur D. Dependency Pairs for Rewriting with No n-free Constructors. In: Pfen- ning F (ed.), Automated Deduction - CADE-21, 21st Internati onal Conference on Automated De- duction, Bremen, Germany, July 17-20, 2007, Proceedings, v olume 4603 of Lecture Notes in Computer Science . Springer, 2007 pp. 426–442. doi:10.1007/978-3-540-7359 5-3\ 32. URL...

    work page doi:10.1007/978-3-540-7359 2007

  12. [12]

    Dependency Pairs for Rewriting with Bu ilt-In Numbers and Semantic Data Structures

    Falke S, Kapur D. Dependency Pairs for Rewriting with Bu ilt-In Numbers and Semantic Data Structures. In: V oronkov A (ed.), Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science . Springer, 2008 pp. 94–109. doi:10.1007/978-3-540-7...

    work page doi:10.1007/978-3-540-70590- 2008

  13. [13]

    Proving Termination in the Conte xt-Sensitive Dependency Pair Framework

    Guti´ errez R, Lucas S. Proving Termination in the Conte xt-Sensitive Dependency Pair Framework. In: ¨Olveczky PC (ed.), Rewriting Logic and Its Applications - 8t h International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Pap ers, volume 6381 of Lecture Notes in Computer Science. Springer, 2010 pp. 18–34. doi:10.1007/97...

    work page doi:10.1007/978-3-642-16310- 2010

  14. [14]

    The 2D Dependency Pai r Framework for conditional rewrite systems

    Lucas S, Meseguer J, Guti´ errez R. The 2D Dependency Pai r Framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci. , 2018. 96:74–106. doi:10.1016/j.jcss.2018. 04.002

    work page doi:10.1016/j.jcss.2018 2018

  15. [15]

    Termination of Generalized Term Rewriting Sys tems

    Lucas S. Termination of Generalized Term Rewriting Sys tems. In: Rehof J (ed.), 9th International Confer- ence on Formal Structures for Computation and Deduction (FS CD 2024), volume 299 of Leibniz Interna- tional Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl, Germany, 2024 pp. 29:1–29:18. doi:10.4230/L...

    work page doi:10.4230/lipics.fscd.2 2024

  16. [16]

    Automatically Proving and Dispr oving Feasibility Conditions

    Guti´ errez R, Lucas S. Automatically Proving and Dispr oving Feasibility Conditions. In: Peltier N, Sofronie-Stokkermans V (eds.), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science . Springer, 2020 pp. 416–435. doi:10.1007/978-3-030-51054-1 27

    work page doi:10.1007/978-3-030-51054-1 2020

  17. [17]

    Fair Conditional Term Rewriting Systems: Uni fication, Termination, and Confluence

    Kaplan S. Fair Conditional Term Rewriting Systems: Uni fication, Termination, and Confluence. In: Kreowski H (ed.), Recent Trends in Data Type Specification, 3 rd Workshop on Theory and Applications of Abstract Data Types, 1984, Selected Papers, volume 116 of Informatik-Fachberichte. Springer, 1984 pp. 136–155. doi:10.1007/978-3-662-09691-8 11

    work page doi:10.1007/978-3-662-09691-8 1984

  18. [18]

    Confluence Framework : Proving Confluence with CONFident

    Guti´ errez R, V´ ıtores M, Lucas S. Confluence Framework : Proving Confluence with CONFident. In: Villanueva A (ed.), Logic-Based Program Synthesis and Tran sformation - 32nd International Symposium, LOPSTR 2022, Proceedings, volume 13474 of Lecture Notes in Computer Science . Springer, 2022 pp. 24–43. doi:10.1007/978-3-031-16767-6 2

    work page doi:10.1007/978-3-031-16767-6 2022

  19. [19]

    Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science

    Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science . Cam- bridge University Press, 2003. ISBN 978-0-521-39115-3

    work page 2003

  20. [20]

    First-Order Logic and Automated Theorem Pro ving, Second Edition

    Fitting M. First-Order Logic and Automated Theorem Pro ving, Second Edition. Graduate Texts in Com- puter Science. Springer, 1996. ISBN 978-1-4612-7515-2. do i:10.1007/978-1-4612-2360-3

    work page doi:10.1007/978-1-4612-2360-3 1996

  21. [21]

    Introduction to mathematical logic (4

    Mendelson E. Introduction to mathematical logic (4. ed .). Chapman and Hall, 1997. ISBN 978-0-412- 080830-7

    work page 1997

  22. [22]

    Confluence of Conditional Rewriting in Logic Form

    Guti´ errez R, Lucas S, V´ ıtores M. Confluence of Conditional Rewriting in Logic Form. In: Boja´ nczy M, Chekuri C (eds.), 41st IARCS Annual Conference on Foundatio ns of Software Technology and Theoret- ical Computer Science (FSTTCS 2021), volume 213 of Leibniz International Proceedings in Informatics (LIPIcs). ISBN 978-3-95977-215-0, 2021 pp. 44:1–44:18...

    work page 2021

  23. [23]

    On Conditional Rewrite Sy stems with Extra V ariables and Deterministic Logic Programs

    Avenhaus J, Lor´ ıa-S´ aenz C. On Conditional Rewrite Sy stems with Extra V ariables and Deterministic Logic Programs. In: Pfenning F (ed.), Logic Programming and Automated Reasoning, 5th International Conference, LP AR’94, Proceedings, volume 822 of Lecture Notes in Computer Science . Springer, 1994 pp. 215–229. doi:10.1007/3-540-58216-9 40

    work page doi:10.1007/3-540-58216-9 1994

  24. [24]

    Completeness Results for Basic Narrowing

    Middeldorp A, Hamoen E. Completeness Results for Basic Narrowing. Appl. Algebra Eng. Commun. Comput., 1994. 5:213–253. doi:10.1007/BF01190830

    work page doi:10.1007/bf01190830 1994

  25. [25]

    Proving and disproving confluence of context-sensitive rewriting

    Lucas S, V´ ıtores M, Guti´ errez R. Proving and disproving confluence of context-sensitive rewriting. Jour- nal of Logical and Algebraic Methods in Programming , 2022. 126:100749. doi:10.1016/j.jlamp.2022. 100749

    work page doi:10.1016/j.jlamp.2022 2022

  26. [26]

    Reliable Confluence Analysis of Condition al Term Rewrite Systems

    Sternagel T. Reliable Confluence Analysis of Condition al Term Rewrite Systems. Ph.D. thesis, Faculty of Mathematics, Computer Science and Physics, University of I nnsbruck, 2017

    work page 2017

  27. [28]

    Modular Properties of Conditional Term R ewriting Systems

    Middeldorp A. Modular Properties of Conditional Term R ewriting Systems. Inf. Comput. , 1993. 104(1):110–158. doi:10.1006/inco.1993.1027

    work page doi:10.1006/inco.1993.1027 1993

  28. [29]

    On the Church-Rosser property for the direct s um of term rewriting systems

    Toyama Y . On the Church-Rosser property for the direct s um of term rewriting systems. J. ACM, 1987. 34(1):128–143. doi:10.1145/7531.7534

    work page doi:10.1145/7531.7534 1987

  29. [30]

    Modularity of Simple Termination of Term Rewriting Systems with Shared Con- structors

    Kurihara M, Ohuchi A. Modularity of Simple Termination of Term Rewriting Systems with Shared Con- structors. Theor . Comput. Sci., 1992. 103(2):273–282. doi:10.1016/0304-3975(92)90015-8

    work page doi:10.1016/0304-3975(92)90015-8 1992

  30. [31]

    Completeness of Combinations o f Constructor Systems

    Middeldorp A, Toyama Y . Completeness of Combinations o f Constructor Systems. J. Symb. Comput. ,

    work page

  31. [32]

    doi:10.1006/JSCO.1993.1024

    15(3):331–348. doi:10.1006/JSCO.1993.1024

    work page doi:10.1006/jsco.1993.1024 1993

  32. [33]

    Modular Properties of Composable Term Rew riting Systems

    Ohlebusch E. Modular Properties of Composable Term Rew riting Systems. J. Symb. Comput. , 1995. 20(1):1–41. doi:10.1006/JSCO.1995.1036

    work page doi:10.1006/jsco.1995.1036 1995

  33. [34]

    On the Modularity of Confluence of Construc tor-Sharing Term Rewriting Systems

    Ohlebusch E. On the Modularity of Confluence of Construc tor-Sharing Term Rewriting Systems. In: Tison S (ed.), Trees in Algebra and Programming - CAAP’94, 19 th International Colloquium, Edinburgh, UK, April 11-13, 1994, Proceedings, volume 787 of Lecture Notes in Computer Science . Springer, 1994 pp. 261–275. doi:10.1007/BFb0017487

    work page doi:10.1007/bfb0017487 1994

  34. [35]

    Modular Properties Of Composable Term Rew riting Systems

    Ohlebusch E. Modular Properties Of Composable Term Rew riting Systems. Ph.D. thesis, FUniversit¨ at Bielefeld, 1994

    work page 1994

  35. [36]

    Operational and Semantic Equiva lence Between Recursive Programs

    Raoult J, Vuillemin J. Operational and Semantic Equiva lence Between Recursive Programs. J. ACM ,

    work page

  36. [37]

    doi:10.1145/322217.322229

    27(4):772–796. doi:10.1145/322217.322229

    work page doi:10.1145/322217.322229

  37. [38]

    Modular Properties Of Term Rewriting Sys tems

    Middeldorp A. Modular Properties Of Term Rewriting Sys tems. Ph.D. thesis, Vrije Universiteit te Ams- terdam, 1990

    work page 1990

  38. [39]

    Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems

    Huet GP . Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM, 1980. 27(4):797–821. doi:10.1145/322217.322230

    work page doi:10.1145/322217.322230 1980

  39. [40]

    The Z-property for left-linear term rewr iting via convective context-sensitive complete- ness

    van Oostrom V . The Z-property for left-linear term rewr iting via convective context-sensitive complete- ness. In: 12th International Workshop on Confluence, IWC 202 3. 2023 pp. 38–43

    work page 2023

  40. [41]

    Unravelings and Ultra-properties

    Marchiori M. Unravelings and Ultra-properties. In: Ha nus M, Rodr´ ıguez-Artalejo M (eds.), Algebraic and Logic Programming, 5th International Conference, ALP’ 96, Aachen, Germany, September 25-27, 1996, Proceedings, volume 1139 of Lecture Notes in Computer Science . Springer, 1996 pp. 107–121. doi:10.1007/3-540-61735-3 7

    work page doi:10.1007/3-540-61735-3 1996

  41. [42]

    On Soundness Con ditions for Unraveling Deterministic Con- ditional Rewrite Systems

    Gmeiner K, Gramlich B, Schernhammer F. On Soundness Con ditions for Unraveling Deterministic Con- ditional Rewrite Systems. In: Tiwari A (ed.), 23rd Internat ional Conference on Rewriting Techniques and Applications (RTA ’12) , RTA 2012, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs). 2012 pp. 193–208. doi:10.4230/LIPIcs.RTA.2012.193

    work page doi:10.4230/lipics.rta.2012.193 2012

  42. [43]

    Soundness of Unravelings f or Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

    Nishida N, Sakai M, Sakabe T. Soundness of Unravelings f or Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity. Log. Methods Comput. Sci. , 2012. 8(3). doi:10.2168/LMCS-8(3: 4)2012

    work page doi:10.2168/lmcs-8(3: 2012

  43. [44]

    Proving Confluence of C onditional Term Rewriting Systems via Unravelings

    Gmeiner K, Nishida N, Gramlich B. Proving Confluence of C onditional Term Rewriting Systems via Unravelings. In: 2nd International Workshop on Confluence, IWC 2013. 2013 pp. 35–39

    work page 2013

  44. [45]

    Level-Confluence of Condi tional Rewrite Systems with Extra V ariables in Right-Hand Sides

    Suzuki T, Middeldorp A, Ida T. Level-Confluence of Condi tional Rewrite Systems with Extra V ariables in Right-Hand Sides. In: Hsiang J (ed.), Rewriting Techniqu es and Applications, 6th International Con- ference, RTA-95, Proceedings, volume 914 of Lecture Notes in Computer Science . Springer, 1995 pp. 179–193. doi:10.1007/3-540-59200-8 56. R. Guti´ errez...

    work page doi:10.1007/3-540-59200-8 1995

  45. [46]

    Generalizing Newman’s Lemma for Le ft-Linear Rewrite Systems

    Gramlich B, Lucas S. Generalizing Newman’s Lemma for Le ft-Linear Rewrite Systems. In: Pfenning F (ed.), Term Rewriting and Applications, 17th Internationa l Conference, RTA 2006, Proceedings, volume 4098 of Lecture Notes in Computer Science . Springer, 2006 pp. 66–80. doi:10.1007/11805618 6

    work page doi:10.1007/11805618 2006

  46. [47]

    Simple Word Problems in Universal A lgebra

    Knuth DE, Bendix PE. Simple Word Problems in Universal A lgebra. In: Leech J (ed.), Computational Problems in Abstract Algebra. Pergamon Press, 1970 pp. 263– 297

    work page 1970

  47. [48]

    Confluence of Condit ional Rewrite Systems

    Dershowitz N, Okada M, Sivakumar G. Confluence of Condit ional Rewrite Systems. In: Kaplan S, Jouan- naud J (eds.), Conditional Term Rewriting Systems, 1st Inte rnational Workshop, Proceedings, volume 308 of Lecture Notes in Computer Science . Springer, 1987 pp. 31–44. doi:10.1007/3-540-19242-5 3

    work page doi:10.1007/3-540-19242-5 1987

  48. [49]

    Conditional Rewrite Rules: Conflu ence and Termination

    Bergstra JA, Klop JW . Conditional Rewrite Rules: Conflu ence and Termination. J. Comput. Syst. Sci. ,

    work page

  49. [50]

    doi:10.1016/0022-0000(86)90033-4

    32(3):323–362. doi:10.1016/0022-0000(86)90033-4

    work page doi:10.1016/0022-0000(86)90033-4

  50. [51]

    Automatic Generation of Logical Models with AGES

    Guti´ errez R, Lucas S. Automatic Generation of Logical Models with AGES. In: Fontaine P (ed.), Automated Deduction - CADE 27 - 27th International Conferen ce on Automated Deduction, Pro- ceedings, volume 11716 of Lecture Notes in Computer Science . Springer, 2019 pp. 287–299. doi: 10.1007/978-3-030-29436-6 17

    work page doi:10.1007/978-3-030-29436-6 2019

  51. [52]

    Prover9 & Mace4

    McCune W . Prover9 & Mace4. Technical report, Universit y of New Mexico, 2005–2010. URL http://www.cs.unm.edu/~mccune/prover9/

    work page 2005

  52. [53]

    FORT 2.0

    Rapp F, Middeldorp A. FORT 2.0. In: Galmiche D, Schulz S, Sebastiani R (eds.), Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Pa rt of the Federated Logic Conference, FloC 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science . Springer, 2018 pp. 81–88. doi: 10.1007/978-3-319-94205-6 6

    work page doi:10.1007/978-3-319-94205-6 2018

  53. [54]

    Data types ` a la carte

    Swierstra W . Data types ` a la carte. J. Funct. Program. , 2008. 18(4):423–436. doi:10.1017/ S0956796808006758

    work page 2008

  54. [55]

    Orthogonality of Generalized Term Rewriting S ystems Submitted to the 13th International Work- shop on Confluence, IWC 2024

    Lucas S. Orthogonality of Generalized Term Rewriting S ystems Submitted to the 13th International Work- shop on Confluence, IWC 2024

    work page 2024

  55. [56]

    Proving Confluence of Term Re writing Systems Automatically

    Aoto T, Y oshida J, Toyama Y . Proving Confluence of Term Re writing Systems Automatically. In: Treinen R (ed.), Rewriting Techniques and Applications, 20 th International Conference, RTA 2009, Proceedings, volume 5595 of Lecture Notes in Computer Science . Springer, 2009 pp. 93–102. doi: 10.1007/978-3-642-02348-4\ 7

    work page doi:10.1007/978-3-642-02348-4 2009

  56. [57]

    CoCo 2020 Participant: ConCon 1.10

    Sternagel C. CoCo 2020 Participant: ConCon 1.10. In: A y ala-Rinc´ on M, Mirmram S (eds.), Proc. of the 9th International Workshop on Confluence, IWC’20. 2020 p. 65

    work page 2020

  57. [58]

    CSI: New Evidenc e - A Progress Report

    Nagele J, Felgenhauer B, Middeldorp A. CSI: New Evidenc e - A Progress Report. In: de Moura L (ed.), Automated Deduction - CADE 26 - 26th International C onference on Automated Deduction, Proceedings, volume 10395 of Lecture Notes in Computer Science . Springer, 2017 pp. 385–397. doi: 10.1007/978-3-319-63046-5 24

    work page doi:10.1007/978-3-319-63046-5 2017

  58. [59]

    CoLL-Saigawa 1.6: A Joint Conflu ence Tool

    Shintani K, Hirokawa N. CoLL-Saigawa 1.6: A Joint Conflu ence Tool. In: Mirmram S, Rocha C (eds.), Proc. of the 10th International Workshop on Confluence, IWC’ 21. 2021 p. 51

    work page 2021

  59. [60]

    CO3: a COnv erter for proving COnfluence of COndi- tional TRSs

    Nishida N, Kuroda T, Y anagisawa M, Gmeiner K. CO3: a COnv erter for proving COnfluence of COndi- tional TRSs. In: 4th International Workshop on Confluence, I WC 2015. 2015 p. 42

    work page 2015

  60. [61]

    Characterizing and provin g operational termination of deterministic con- ditional term rewriting systems

    Schernhammer F, Gramlich B. Characterizing and provin g operational termination of deterministic con- ditional term rewriting systems. J. Log. Algebraic Methods Program. , 2010. 79(7):659–688. doi: 10.1016/j.jlap.2009.08.001. 216 R. Guti´ errez et al./ Proving Confluence with CONFident

    work page doi:10.1016/j.jlap.2009.08.001 2010

  61. [62]

    Hakusan 0.8: A Confluence Tool

    Shintani K, Hirokawa N. Hakusan 0.8: A Confluence Tool. I n: 12th International Workshop on Conflu- ence, IWC 2023. 2023 p. 65

    work page 2023

  62. [63]

    Compositional Confluence Criteria

    Shintani K, Hirokawa N. Compositional Confluence Crite ria. In: Felty AP (ed.), 7th International Confer- ence on Formal Structures for Computation and Deduction, FS CD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of Leibniz International Proceedings in Informatics (LIPIcs ). Schloss Dagstuhl - Leibniz- Zentrum f¨ ur Informatik, 2022 pp. 28:1–28:19. d...

    work page doi:10.4230/lipics.fscd.2022.28 2022

  63. [64]

    CoCo 2023 Participant: ConfCSR

    Stevanovic F, Mitterwallner F. CoCo 2023 Participant: ConfCSR. In: 12th International Workshop on Confluence, IWC 2023. 2023 p. 63

    work page 2023

  64. [65]

    Cell Types, Network Homeostasis, and Pathological Compensation from a Biologically Plausible Ion Channel Expression Model

    Lucas S. Proving semantic properties as first-order sat isfiability. Artif. Intell., 2019. 277. doi:10.1016/j. artint.2019.103174

    work page doi:10.1016/j 2019

  65. [66]

    Complete Sets of Reductions fo r Some Equational Theories

    Peterson GE, Stickel ME. Complete Sets of Reductions fo r Some Equational Theories. J. ACM, 1981. 28(2):233–264. doi:10.1145/322248.322251

    work page doi:10.1145/322248.322251 1981

  66. [67]

    Nominal rewriting

    Fern´ andez M, Gabbay M. Nominal rewriting. Inf. Comput. , 2007. 205(6):917–965. doi:10.1016/J.IC. 2006.12.002. URL https://doi.org/10.1016/j.ic.2006.12.002

    work page doi:10.1016/j.ic 2007

  67. [68]

    On the Church-Rosser and coherenc e properties of conditional order-sorted rewrite theories

    Dur´ an F, Meseguer J. On the Church-Rosser and coherenc e properties of conditional order-sorted rewrite theories. J. Log. Algebraic Methods Program., 2012. 81(7-8):816–850. doi:10.1016/j.jlap.2011.12.004

    work page doi:10.1016/j.jlap.2011.12.004 2012

  68. [69]

    Confluent and Coherent Equational Term Rew riting Systems: Application to Proofs in Abstract Data Types

    Jouannaud J. Confluent and Coherent Equational Term Rew riting Systems: Application to Proofs in Abstract Data Types. In: Ausiello G, Protasi M (eds.), CAAP’ 83, Trees in Algebra and Programming, 8th Colloquium, Proceedings, volume 159 of Lecture Notes in Computer Science. Springer, 1983 pp. 269–283. doi:10.1007/3-540-12727-5 16

    work page doi:10.1007/3-540-12727-5 1983

  69. [70]

    Completion of a Set of Rules Mod ulo a Set of Equations

    Jouannaud J, Kirchner H. Completion of a Set of Rules Mod ulo a Set of Equations. SIAM J. Comput. ,

    work page

  70. [71]

    doi:10.1137/0215084

    15(4):1155–1194. doi:10.1137/0215084

    work page doi:10.1137/0215084

  71. [72]

    Ground Confluence and Strong Commutation Mod ulo Alpha-Equivalence in Nominal Rewrit- ing

    Kikuchi K. Ground Confluence and Strong Commutation Mod ulo Alpha-Equivalence in Nominal Rewrit- ing. In: Seidl H, Liu Z, Pasareanu CS (eds.), Theoretical Asp ects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27 -29, 2022, Proceedings, volume 13572 of Lec- ture Notes in Computer Science . Springer, 2022 pp. 255–271...

    work page doi:10.1007/978-3-031-1771 2022

  72. [73]

    Confluence and Commutation for Nomina l Rewriting Systems with Atom-V ariables

    Kikuchi K, Aoto T. Confluence and Commutation for Nomina l Rewriting Systems with Atom-V ariables. In: Fern´ andez M (ed.), Logic-Based Program Synthesis and T ransformation - 30th International Sympo- sium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Pro ceedings, volume 12561 of Lecture Notes in Computer Science . Springer, 2020 pp. 56–73. doi:10.1...

    work page doi:10.1007/978-3-030-68446- 2020

  73. [74]

    Confluence of Conditional Rewriting Modulo

    Lucas S. Confluence of Conditional Rewriting Modulo. In : Murano A, Silva A (eds.), 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), vol ume 288 of Leibniz International Pro- ceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl, Germany. ISBN 978-3-95977-310-2, 2024 pp. 37:1–37:21. doi:10.4230 /L...

    work page 2024

  74. [75]

    Order-Sorted Algebra I: Equatio nal Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations

    Goguen JA, Meseguer J. Order-Sorted Algebra I: Equatio nal Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theor . Comput. Sci. , 1992. 105(2):217–273. doi: 10.1016/0304-3975(92)90302-V. R. Guti´ errez et al./ Proving Confluence with CONFident 217 A. Proof of Proposition 5.3 Proposition 5.3 LetR = (F, Π, µ, H, R) be a GT...

    work page doi:10.1016/0304-3975(92)90302-v 1992

  75. [76]

    If s→ R t, then s→ ∗ Rα,x,i t

    work page

  76. [77]

    Proof: As for the first claim (s→ R t implies s→ ∗ Rα,x,i t), by using the version for GTRSs of [1, Theorem 10] for CTRSs (see [1, Section 7.5]), s→ R t iff R⊢ s↓→ t↓

    If s→ Rα,x,i t, then s→ R t. Proof: As for the first claim (s→ R t implies s→ ∗ Rα,x,i t), by using the version for GTRSs of [1, Theorem 10] for CTRSs (see [1, Section 7.5]), s→ R t iff R⊢ s↓→ t↓. We proceed by induction on the length n≥ 0 of a Hilbert-like proof of s↓→ t↓ fromR. Base: n = 0. With s↓→ t↓ we are using (HC)α for some unconditional rule α : ℓ...

    work page

  77. [78]

    Then, s↓ = f (s1,

    A sentence (Pr)f,i is used for some f∈F and i∈ µ (f ). Then, s↓ = f (s1, . . . , s i, . . . , s k) and t↓ = f (s1, . . . , t i, . . . , s k) for some (ground) terms s1, . . . , s k and ti and R⊢ si→ ti has been proved in less than n steps. By the induction hypothesis, Rα,x,i ⊢ si→ ti holds as well. Thus, by using again (Pr)f,i (which is part ofRα,x,i ), w...

    work page

  78. [79]

    If β̸= α , then β is also a rule ofRα,x,i and by using the induction hypothesis, we conclude s↓→ Rα,x,i t↓

    A sentence (HC)β has been used for some β∈ R. If β̸= α , then β is also a rule ofRα,x,i and by using the induction hypothesis, we conclude s↓→ Rα,x,i t↓. Otherwise, β = α and s↓ = ς(ℓ) and t↓ = ς(r) for some substitution ς, and also (by the induction hypothesis and because α is an O-rule), for all 1≤ j≤ n, ς(sj)→ ∗ Rα,x,i ς(tj) (50) InRα,x,i for σ = {x ↦→...

    work page

  79. [80]

    Analogous to the corresponding case of the first claim

    A sentence (Pr)f,i is used for some f∈F and i∈ µ (f ) . Analogous to the corresponding case of the first claim

    work page

  80. [81]

    If β̸= α x,i , then β∈ R; hence s↓→ R t↓

    A sentence (HC)β has been used for some conditional rule β . If β̸= α x,i , then β∈ R; hence s↓→ R t↓. Otherwise, if β = α x,i , then s↓ = ς(ℓ)→ Rα,x,i ς(r[s]P ) = t↓ for some substitution ς such that ς(sj[s]Pj )→ ∗ Rα,x,i ς(tj) holds for all 1≤ j≤ n, j̸= i. By the induction hypothesis (and repeatedly using (Co) and (Rf)), ς(sj[s]Pj )→ ∗ R ς(tj) holds for...

    work page