Termination and Confluence of Higher-Order Rewrite Systems
在过去的20年里，已经提出了几种高阶重写方法，其中包括Klop的组合重写系统（CRS），Nipkow的高阶重写系统（HRS）以及Jouannaud和Okada的高阶代数规约语言，其中只有最后一种考虑了类型化项。Jouannaud、Okada和本文作者将后一种方法推广到归纳数据类型系统（IDTS）。在本文中，我们扩展了IDTS与CRS高阶模式匹配机制，导致简单类型的CRS。然后，我们展示了如何终止标准开发的IDTS与一阶模式匹配，称为一般模式，可以扩展，以证明强规范化的IDTS与高阶模式匹配。接下来，我们将统一的方法与HRS进行比较。我们首先证明了扩展的一般模式也可以适用于人力资源系统。其次，我们展示了如何Nipkow的高阶临界对分析技术证明当地的融合可以应用于IDTS。
2006-10-11 cs.LO
Automated Strategy Invention for Confluence of Term Rewrite Systems
University of Innsbruck（因斯布鲁克大学）；Shanghai Jiao Tong University（上海交通大学）；Czech Technical University in Prague（布拉格捷克技术大学）；University of Melbourne（墨尔本大学）
针对项重写系统合流性证明中参数选择复杂的问题，研究者用机器学习构建首个学习引导的自动合流性证明器，生成大型数据集，改进的CSI证明器性能超越人工策略，解决了此前无自动证明的若干问题。
2025-07-31 cs.AI cs.LO
Confluence of Layered Rewrite Systems
我们研究了新的，图灵完备类的分层系统，其左手边的规则只能重叠在一个多集的不相交或相等的位置。分层系统定义了一个自然的术语等级概念：沿着从根到叶的路径的非重叠赎回的最大数量。在有限或无限树中允许重叠。规则可以是非终止的、非左线性的或非右线性的。使用一种新的统一技术，循环统一，和所谓的subrewriting关系，我们证明了秩非增层系统是合流的，只要他们的循环临界对有循环可连接的下降图。
2015-09-15 cs.LO
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
线性-代数演算和代数演算是用任意线性组合项扩展的无类型代数代数演算。前者以重写系统的形式呈现线性代数的公理，而后者使用等式。当重写时，代数演算不是融合的，除非增加进一步的限制。我们提供了一个类型系统的线性代数演算强制执行强规范化，这给回汇合。类型系统允许在系统F中进行抽象解释。
2012-03-28 cs.LO
Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
Graduate School of Informatics, Nagoya University（名古屋大学情报大学院）
本文提出在逻辑约束重写中扩展重写归纳方法，以处理存在量词方程，通过引入存在量词到方程和规则中，实现对约束方程的归纳证明。
2026-02-16 cs.LO
Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
针对基础项重写系统，提出高效判定NFP、UNR、UNC和CR的算法，分别达到三次、近三次、近线性和三次时间复杂度，改进先前界限。
2018-10-26 cs.FL cs.LO
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
我们给出了一种方法来证明包含非终止重写规则（如交换性和结合性）的项重写系统的汇流性。通常，包含这些规则的项重写系统的汇流性通过将它们视为等式项重写系统并考虑E-临界对和/或终止模E来证明。相比之下，我们的方法仅基于通常的临界对，即使系统不终止模E，它也（部分）起作用。我们首先提出的合流标准，长期重写系统的重写规则可以划分为一个终止的部分和可能的非终止的部分。然后我们给出了一个保持约简的完备化过程，从而增强了准则的适用性。与著名的Knuth-Benzmann完备化过程保持系统的等价关系不同，我们的完备化过程保持系统的约化关系，从而从完备化系统的收敛性推导出原系统的收敛性.
2012-03-27 cs.LO
Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version)
本文扩展了模式差运算符和补集算法至逻辑约束项重写系统（LCTRSs）的约束线性模式，证明带可判定内置理论的左线性LCTRSs的拟可约性可判定，且约束模式差运算仅要求除数模式线性。
2025-07-08 cs.LO
Compositional Confluence Criteria
本文将基于递减图的汇合性判据推广为可组合形式，并应用于项重写中的正交性、规则标号和临界对系统，同时提出移除不必要重写规则的归约方法，并证明 Toyama 并行封闭性结果蕴含几乎并行封闭性定理。
2024-01-22 cs.LO
Confluence by Critical Pair Analysis Revisited (Extended Version)
我们提出了两种方法来证明左线性项重写系统的合流性。一个是热递减，结合并行/开发封闭性定理与基于终止子系统的规则标签。另一种是临界对闭系统，它将汇流问题归结为一个特殊子系统的汇流问题，该子系统的复制规则是相对终止的。
2019-06-03 cs.LO cs.SC
Labelings for Decreasing Diagrams
这篇文章关注的是自动化vanOostrom的递减图技术，用于建立术语重写系统的汇合。我们研究抽象的标准，允许字典结合标签，以显示当地的图表减少。这种方法有两个直接的好处。首先，只要满足一些温和的条件，它允许对线性重写系统使用标记，也允许对左线性重写系统使用标记。第二，它承认一个增量的方法证明融合，其中包括最近的发展，自动减少图。文章中提出的技术已经实现，实验结果表明，例如，规则标签得益于我们的贡献。
2014-10-09 cs.LO
On the Verification of Logically Decorated Graph Transformations
我们解决的问题，推理图转换功能的行动，如\emph{addition}和\emph{deletion}的节点和边缘，节点\emph{merging}和\emph{cloning}，节点或边缘\emph{labelling}和边缘\emph{redirection}。首先，我们介绍了所考虑的图重写系统参数化的一个给定的逻辑$\mathcal{L}$。利用$\mathcal{L}$的公式对图的节点和边进行标记。在第二步中，我们解决的问题，所考虑的重写系统的形式验证，通过使用霍尔最弱的前提演算。它作用于$\{\texttt{Pre}\}(\texttt{R},\texttt{strategy}) \{\texttt{Post}\}$形式的三元组，其中\texttt{Pre}和\texttt{Post}是在给定逻辑$\mathcal{L}$中指定的条件，\texttt{R}是图形重写系统，而\texttt{strategy}是说明如何执行\texttt{R}中的规则的表达式。我们证明我们介绍的微积分是健全的。此外，我们展示了如何建议的框架可以成功地实例化不同的逻辑。我们调查一阶逻辑和它的几个可判定的片段，特别侧重于不同方言的描述逻辑（DL）。我们还表明，通过使用互模拟关系，一些DL片段不能使用，由于他们缺乏表达能力。
2018-03-07 cs.LO
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
本文提出了一种新的最一般约束重写方法，使逻辑约束重写与等价变换可交换，从而解决实现中的搜索空间问题。
2025-12-15 cs.LO
Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
本文研究逻辑约束项重写的语义，定义受约束等式、等式理论及有效性，构建可靠推理系统并提出代数语义以判定无效性和新的一致性概念。
2024-07-05 cs.LO
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
在本文中，我们提出了一种新的方法，一个命令式程序的函数调用和全局变量转换成一个逻辑约束的长期重写系统。所得到的系统用调用堆栈表示整个执行环境的转换。更准确地说，我们为整个环境准备了一个函数符号，它存储全局变量的值和一个调用堆栈作为其参数。对于一个函数调用，我们准备重写规则来将帧压入堆栈，并在执行后弹出它。任何运行的框架都位于堆栈的顶部，访问全局变量的语句由环境符号的重写规则表示。我们展示了一个精确的转换的基础上的方法，并证明其正确性。
2019-02-22 cs.LO cs.PL
Proving Confluence in the Confluence Framework with CONFident
Universidad Politécnica de Madrid（马德里理工大学）；Universitat Politècnica de València（瓦伦西亚理工大学）
本文介绍Confluence框架，用于通过分而治之的模块化策略证明和反驳连通性，并在CONFident中实现。该方法能自动证明和反驳广义项重写系统的连通性，包括选择性重写函数符号的参数和一般条件规则。
2024-08-28 cs.LO cs.PL
Uniqueness of Normal Forms for Shallow Term Rewrite Systems
范式的唯一性（$UN^=$）是项重写系统的一个重要性质。$UN^=$对于地是可判定的（即，无变量）系统和一般不可判定。最近，它被证明是可判定的线性，浅系统。我们推广了以前的结果，并表明，这个属性是可判定的浅重写系统，在相反的汇合，可达性和其他属性，这都是不可判定的平面系统。我们的结果在某种意义上也是最优的，因为我们证明了$UN^=$属性对于两类线性重写系统是不可判定的：左手边深度至多为2的左平坦系统和左手边深度至多为2的右平坦系统。
2016-07-01 cs.FL cs.LO
On Complexity Bounds and Confluence of Parallel Term Rewriting
LIP (UMR CNRS/ENS Lyon/UCB Lyon1/Inria)（LIP（法国国家科学研究中心/里昂高等师范学院/里昂第一大学/法国国家信息与自动化研究所联合研究单位））；Birkbeck, University of London（伦敦大学伯贝克学院）；University Grenoble Alpes（格勒诺布尔阿尔卑斯大学）
本文研究并行内最重写模型的复杂度界限与连通性，提出自动技术推导并行重写复杂度的上下界，通过扩展AProVE工具验证方法的有效性。
2024-09-02 cs.LO cs.PL
Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)
Niigata University（新潟大学）；Nagoya University（名古屋大学）；Data Lab Hell
本文提出部分约束重写与价值解释，用于分析逻辑约束项重写系统中不同重写方法的差异及特性。
2026-10-27 cs.LO
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
有限项和无穷项重写理论在正交重写系统中得到了广泛的发展，但在弱正交重写系统中的发展程度较低。在本文中，我们提出了一些贡献，后者的情况下，弱正交性，临界对被接纳，只要他们是平凡的。我们开始与现在经典的压缩引理，作为一种工具，建立无穷汇流，因此独特的无穷范式的属性，弱正交TRS的情况下，不包含折叠重写规则的细化。这种限制的无重叠是至关重要的，是在一个简单的TRS的阐述是弱正交的，但有两个崩溃的规则。事实证明，所有通常的理论都戏剧性地崩溃了。最后，我们建立了一个积极的事实：钻石性质的无限发展弱正交TRS，通过详细的分析，由范奥斯特罗姆有限的情况下。
2009-11-05 cs.LO
Runtime Complexity Analysis of Logically Constrained Rewriting
逻辑约束重写系统（LCTRS）是一种通用且高效的重写形式主义，可用于从各种编程范式建模程序，以及编译器和SMT求解器中的简化系统。在本文中，我们研究技术来分析最坏情况下的运行时复杂性的LCTRS。为此，我们利用以前开发的分解技术之间的协同作用，由Avanzini等人重写的标准项。与交替的时间和大小的整数程序的边界近似Brockschloven等人。并适应这些技术适当的LCTRS。此外，我们提供了新的模块化技术，利用循环边界的递归方程，产生次线性边界。我们已经实现了TCT的方法来测试我们的方法的可行性。
2020-12-11 cs.CC cs.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
Confluence of conditional rewriting modulo
本文研究了条件重写系统中模E的重写交汇性，提出基于逻辑和参数条件对的新方法，适用于等式术语重写系统。
2026-07-31 cs.LO cs.PL cs.SC
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
本文针对带位向量算术的逻辑约束项重写系统，提出一种基于有向无环图的依赖对处理器，以解决单例自环依赖对问题，并给出无环图存在的充分条件及特定情况下的简化。
2023-07-26 cs.LO
Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity
King’s College London（伦敦国王学院）；Univ. Artois, CNRS, Centre de Recherche en Informatique de Lens (CRIL)（阿图瓦大学、法国国家科学研究中心、伦斯信息学研究中心）
本文研究了通过语法重写规则最小化逻辑等价句子宽度的问题，提出了一个算法以确定给定正则一阶句子在应用规则后的最小宽度句子，填补了该领域通用设置下的空白。
2026-04-15 cs.DB cs.LO
