Sparse Tiling through Overlap Closures for Termination of String Rewriting
我们在字符串重写中过度近似可达集，这是由可接受因子（称为瓦片）定义的语言。一个稀疏的瓦片集只包含那些在派生中可到达的瓦片，并且通过完成自动机来构造。利用语义标记的稀疏分片定义的部分代数，我们得到了一个证明局部终止性的变换方法。利用前向闭包的已知结果和重叠闭包的新特征，我们分别获得了证明终止性和相对终止性的方法。我们报告显示这些方法的强度的实验。
2020-03-03 cs.LO
Size-based termination of higher-order rewriting
我们提供了一个通用的和模块化的标准终止简单类型的$λ$ -演算扩展的功能符号定义的用户定义的重写规则。根据Hughes、Pareto和Sabry对使用定点运算符和模式匹配定义的函数的研究，有几个标准使用类型规则来限制函数调用中参数的高度。在本文中，我们将这种方法扩展到基于重写的函数定义和更一般的用户定义的大小概念。
2018-02-20 cs.LO
From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity
本文提出在概率术语重写系统中，通过分析最内重写下的几乎确定终止来证明完整终止，并探讨其复杂性与模块性。
2025-12-11 cs.LO
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
本文将依赖对技术扩展到概率项重写系统，提出带标注依赖对框架以自动证明完全与最内层重写下的几乎必然终止性，并在 AProVE 中实现验证。
2025-06-05 cs.LO
Non-Termination in Term Rewriting and Logic Programming
本文在统一框架下定义循环与二元链两种非终止形式，提出检测二元链的语法判据，并通过NTI在2023年终止竞赛中与领先分析器比较验证其有效性。
2023-12-21 cs.LO
Termination of Rewriting with and Automated Synthesis of Forbidden Patterns
我们介绍了一个修改后的版本，著名的依赖对框架，是适合于禁止模式限制下的重写终止分析。通过将上下文附加到表示相应递归函数调用的调用上下文的依赖对，可以将禁止模式限制合并到依赖对链的（适应的）概念中，从而产生可靠且完整的终止分析方法。建立在这个上下文依赖对框架，我们引入了一个依赖对处理器，通过分析依赖对的上下文信息，简化了问题。此外，我们展示了如何使用这个处理器来合成禁止模式适合于一个给定的长期重写系统的飞行在终止分析。
2010-12-27 cs.LO
Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
本研究将依赖对框架适配至概率场景，提出用于证明概率项重写系统几乎必然最内层终止的依赖元组方法，并在工具AProVE中实现以验证其效力。
2023-07-19 cs.LO
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
本文将经典依赖对框架扩展至概率项重写系统，用于证明几乎必然最内层终止性，并在 AProVE 工具中实现以验证其能力。
2023-06-03 cs.LO
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
2025-10-15 cs.LO
Termination of Rewriting with Right-Flat Rules Modulo Permutative Theories
我们提出了可判定性的结果终止类的长期重写系统模置换理论。终端和最里面的终止模置换理论被证明是可判定的长期重写系统（TRS），其右手边的条款被限制为浅（变量发生在深度最多一个）和线性（每个变量发生在最多一次）。最内层终止模置换理论也被证明是可判定的浅TRS。我们首先表明，一个浅TRS可以转化为一个平面（只有变量和常数发生在深度1）TRS，同时保持终止和最内层终止。然后证明了可判定性的结果表明：（a）右平坦右线性（平坦）TRS，非终止（分别，最内非终止）意味着从平坦项开始的非终止，和（b）右平坦TRS，从给定项开始的非终止导子的存在是可判定的。在消极的一面，我们显示PSPACE-硬的终止和最内终止浅右线性TRS，和undecidability终止平坦的TRS。
2010-08-25 cs.LO
Transforming Outermost into Context-Sensitive Rewriting
我们定义了两个转换从长期重写系统（TRS）上下文敏感的TRS在这样一种方式，即终止的目标系统意味着最外层终止的原始系统。在基于“上下文扩展”的转换中，每个最外面的重写步骤都由转换后的系统中的一个步骤来建模。这个转换原来是完整的左线性TRS类。第二个转换被称为“动态标记”，并导致更小尺寸的上下文敏感的TRS。在这里，每个建模步骤都与少量辅助步骤相邻。因此，国家的最先进的上下文敏感的重写终止方法成为可用于证明终止最外层重写。这两种转换都已在Jambox中实现，使其成为最后一版年度终止竞争的最外层重写类别中最成功的工具。
2010-06-29 cs.LO
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
RWTH Aachen University（亚琛工业大学）
本文提出首个自动反驳概率项重写系统（正）几乎必然终止性的技术，通过将随机游走嵌入计算来定量分析循环的存在性和计数。
2026-05-28 cs.LO
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。
2025-01-22 cs.LO
Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms
本文针对概率重写系统，研究结果唯一性（唯一极限分布），提出证明技术以分析和比较归约策略，为概率演算的操作性分析提供工具。
2022-04-25 cs.LO
Termination of LCTRSs
逻辑约束项重写系统（LCTRS）提供了一个通用的框架与约束项重写。我们讨论了一个简单的依赖对的方法来证明终止LCTRS。我们看到，现有的技术以自然的方式转移到受约束的设置。
2016-01-13 cs.LO
A Dependency Pair Framework for Relative Termination of Term Rewriting
本文提出了一种新型的标注依赖对（ADPs）框架，用于证明项重写系统的相对终止，并在工具AProVE中实现，对比现有工具展现了其有效性。
2024-04-23 cs.LO
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
本文针对概率项重写系统的 iAST 问题，重新定义依赖对并引入新转换，将不完备的依赖元组方法发展为完备的概率 DP 框架，且在 AProVE 中验证其证明能力显著提升。
2024-02-29 cs.LO
Rewriting modulo in Deduction modulo
我们研究的终止重写模一组方程的代数构造演算，扩展的构造演算的功能和谓词定义的高阶重写规则。在以前的工作中，我们定义了一般的语法条件的基础上的概念，可计算的闭包，以确保终止的组合重写和β-减少。在这里，我们表明，这一结果是保留时，考虑重写模一组方程，如果这些方程产生的等价类是有限的，方程是线性的，并满足一般的语法条件，也基于可计算闭包的概念。这包括方程，如结合性和交换性，并提供了一个原始的处理终止模方程。
2006-10-11 cs.LO
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
在以前的工作中，第一作者扩展到高阶重写和依赖类型中使用类型中的大小注释，这是一种终止证明技术，称为基于类型或大小的终止，最初为ML类程序开发。在这里，我们通过考虑条件重写和显式量化以及对大小注释的约束更进一步。这允许更精确地描述函数输出的大小如何取决于其输入的大小。因此，我们可以检查更多函数的终止。首先给出了一个基于约束求解的通用类型检测算法。然后，我们给出了Presburger算法中的一个带约束的终止准则。据我们所知，这是高阶条件重写的第一个终止准则，考虑到终止的条件。
2006-09-11 cs.LO
Type theory and rewriting
我们研究的属性，特别是终止，依赖类型系统的λ演算和重写。
2007-02-22 cs.LO
Termination orders for 3-dimensional rewriting
本文研究了3-测谎仪作为一个框架重写的二维词。将项重写系统转化为具有显式资源管理的3-polygraphs，并研究了每个系统的计算性质。最后，给出了Z/2 Z-向量空间（交换）理论的收敛3-多道图。为了证明这些结果，它是解释如何手工制作一类终止订单的3-多道。
2006-12-04 cs.LO math.CT
Polygraphs for termination of left-linear term rewriting systems
利用Albert Burroni的多道生理记录图证明了左线性项重写系统（TRS）的终止性。我们将所考虑的TRS转换成一个最小尺寸的测谎仪，其终止性是用测谎仪解释证明的，然后我们回到TRS上的属性。我们回顾伊夫拉丰的一般翻译的TRS到测谎仪和已知的链接之间的终止属性。我们给出了几个条件的原始TRS，包括作为一个一阶函数程序，以确保我们可以减少的多道转换的大小。我们还证明了充分条件的最小的翻译，意味着终止原来的TRS的polygraphic解释。最后给出了与通常的多项式解释方法相比较的例子。
2007-02-07 cs.LO math.CT
Proving Looping and Non-Looping Non-Termination by Finite Automata
提出了一种新的证明项重写非终止性的方法。其基本思想是找到一个非空的项的正则语言，它在重写下是封闭的，并且不包含范式。它是自动化的，用一个有固定数量状态的树自动机来表示语言，并用SAT公式来表达上述要求。这个公式的可满足性意味着不终止。我们的方法成功的许多例子，所有早期的技术失败，例如从组合逻辑的S规则。
2015-05-03 cs.LO
Polynomial Interpretations for Higher-Order Rewriting
弱单调代数的终止方法，在HRS形式主义中被定义为高阶重写，提供了很大的力量，但近年来很少使用。我们适应和扩展这种方法的替代形式主义的代数功能系统，其中简单类型的代数演算与代数约简相结合。使用这一理论，我们定义高阶多项式的解释，并显示如何实现这种技术的挑战可以解决。终止工具WANDA中提供了完整的实现。
2012-03-26 cs.LO
An Automated Approach to the Collatz Conjecture
我们探讨Collatz猜想及其变种通过终止字符串重写的镜头。我们构建了一个重写系统，模拟迭代应用Collatz函数对应的混合二元-三元表示的正整数字符串。我们证明了这个重写系统的终止等价于Collatz猜想。我们还证明，以前研究的重写系统，模拟Collatz函数使用一元表示不承认终止证明，通过自然矩阵的解释，即使使用依赖对。为了证明我们的方法在数学上有趣的语句的可行性，我们实现了一个最小的终止证明，使用自然/北极矩阵的解释，我们发现自动化证明的非平凡的削弱Collatz猜想。虽然我们没有成功地证明Collatz猜想，我们相信，这里的想法代表了一个有趣的新方法。
2022-12-31 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
Formalizing the Dependency Pair Criterion for Innermost Termination
重写是一个推理函数式编程的框架。依赖对准则是一种众所周知的分析术语重写系统终止的机制。在重写框架中，具有基于评估的操作语义的功能规范与最内层的归约关系相关。本文给出了最内层约简关系的依赖对准则的PVS形式化：一个项重写系统是最内层可终止的当且仅当它被依赖对准则终止。本文还讨论了该准则在功能规格说明终止性检查中的应用。
2019-10-30 cs.LO cs.PL
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
Non-termination using Regular Languages
我们描述了一种方法来证明非循环不终止，即长期重写系统不承认循环减少。作为非终止证书，我们采用常规（树）自动机。
2014-05-22 cs.LO
Certifying Higher-Order Polynomial Interpretations
本文提出一种认证高阶项重写系统终止性证明的方法，通过形式化多项式解释方法，并将终止性分析工具Wanda的输出转换为Coq脚本以验证证明的有效性。
2023-08-05 cs.LO
Non-simplifying Graph Rewriting Termination
LORIA（洛林信息学及其应用研究实验室）；Université de Lorraine（洛林大学）；Inria Nancy Grand-Est（法国国家信息与自动化研究所南锡大东部中心）
到目前为止，自然语言处理（NLP）中的大量工作依赖于树作为核心数学结构来表示语言信息（例如Chomsky的工作）。然而，有些语言现象并不能很好地处理树。在以前的论文中，我们展示了用图来编码语言结构和使用图重写规则来计算这些结构的好处。出于一些语言学上的考虑，图重写的特征在于两个特征：第一，沿着计算没有节点创建，第二，有非局部边修改。在这些假设下，我们证明了一致终止是不可判定的，非一致终止是可判定的。我们描述了两个终止技术的基础上的重量，我们给这些重写系统的推导长度的复杂性界。
2013-02-26 cs.CC cs.CL cs.LO
Termination of rewrite relations on $λ$-terms based on Girard's notion of reducibility
本文将Girard为证明多态$λ$ -演算中的$β$ -约简的终止性而引入的约简概念加以推广，利用可计算闭包的概念证明了$λ$ -项上的各种重写关系的终止性，包括模某些方程理论的重写和匹配模$β$ $η$的重写.这为各种高阶重写框架提供了一个强大的终止准则，包括Klop的简单类型组合约简系统和Nipkow的高阶重写系统。
2015-09-02 cs.LO math.LO
Hydra Battles and AC Termination
本文提出用带AC符号的重写系统编码赫拉克勒斯与九头蛇之战，可忠实建模任意策略，并通过类型引入、多类型语义标签和新的AC-MPO归约序证明其终止性。
2025-06-25 cs.LO
Termination of canonical context-sensitive rewriting and productivity of rewrite systems
程序的终止，即，不存在无限的计算，确保了所有初始表达式的范式的存在，从而为函数式程序的规范化语义的定义提供了必要的成分。然而，在惰性函数式语言中，无限的数据结构通常作为计算的结果来交付。例如，所有素数的列表可以作为数值表达式或数据结构的永不结束的流返回。如果允许这样的流，要求终止是无望的。在这种情况下，生产力的概念可以用来提供一个无限数据结构计算的帐户，因为它“捕捉了可计算性的概念，无限列表程序的进展”（B.A. Sijtsma，On the Productivity of Recursive List Definitions，ACM Transactions on程序设计语言and Systems 11（4）：633-649，1989）。然而，在领域的长期重写系统，这可以被看作是（一阶，无类型，无条件）的功能程序，上下文敏感重写（CSR）的终止已被证明相当于重写系统的生产力，通过适当的转换。通过这种方式，可以使用证明CSR终止的工具来证明生产力。在术语重写中，CSR是当仅允许对函数符号的选定参数进行约简时产生的重写限制。在本文中，我们表明，众所周知的CSR的计算能力的结果是有用的，以更好地了解现有的重写系统的生产力和终止CSR之间的联系，并获得更强大的技术来证明重写系统的生产力。
2015-12-22 cs.LO cs.PL
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem
本文将一类表现力等同经典电路的可逆布尔电路表示为自由3-范畴Toff，通过定义到3-范畴Move的非保恒等函子追踪导线移动，从而证明电路重写的终止性。
2024-01-04 cs.LO math.CT
Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings
本文提出基于有序半环的加权类型图方法，将矩阵解释推广到图重写，通过权重递减证明图变换系统的均匀终止性，并在工具Grez中实现。
2023-10-11 cs.FL cs.LO
Bounded Rewriting Induction for LCSTRSs
Radboud University（拉德堡德大学）
本文提出有界重写归纳方法，通过减少终止要求来提升LCSTRSs中的归纳证明能力。
2026-11-06 cs.LO
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
2006-10-11 cs.LO cs.PL
A Formalization of Abstract Rewriting in Agda
Appalachian State University（阿巴拉契亚州立大学）
本文在Agda中形式化了抽象重写系统，改进了终止和连通性标准，并通过lambda演算示例展示了其应用。
2026-03-11 cs.LO math.LO
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
2008-09-01 cs.AI cs.LO cs.PL
The unified higher-order dependency pair framework
近年来，针对一阶项重写终止性分析的强大依赖对方法，定义了两种高阶扩展：静态方法和动态方法。这两种方法都有明显的优点和缺点。然而，一个大统一的理论是迄今为止失踪，这两种方法缺乏模块化的依赖对框架中常用的一阶重写。此外，这两种方法都不能用来证明不终止。在本文中，我们的目标是通过定义一个高阶依赖对框架，将这两种方法集成到一个共享的正式设置来解决这个差距。该框架已在（全自动）高阶终止工具WANDA中实现。
2018-05-23 cs.LO
Formalizing Higher-Order Termination in Coq
我们描述了高阶重写理论的形式化，并正式证明了AFS是强规范化的，如果它可以解释在一个良好的基础域。为此，我们使用Coq，它是一个基于依赖类型论的证明助手。使用这种形式化，可以实现几种终止技术，如解释方法或依赖对，并证明它们的正确性。然后可以将这些实现提取到OCaml中，这会产生经过验证的终止检查器。
2021-12-13 cs.LO
Higher-Order Constrained Dependency Pairs for (Universal) Computability
本文将静态依赖对框架适配至逻辑约束简单类型项重写系统（LCSTRSs），并提出通用可计算性概念以实现开放世界终止性分析。
2024-07-30 cs.LO
Strategies for linear rewriting systems: link with parallel rewriting and involutive divisions
我们研究重写系统，其底层的条款集配备了一个向量空间结构在一个给定的字段。我们引入并行重写关系，这是重写关系兼容的向量空间结构，以及重写策略，其中包括在选择一个重写步骤，为每个可约的基础元素的向量空间。使用这些概念，我们介绍了S-合流性质，并表明它意味着合流。我们推导出钻石引理的证明，基于战略。我们说明了我们的一般框架重写系统的有理外尔代数，这是向量空间的一个领域的有理函数。特别是，我们表明，对合部门诱导重写策略的有理Weyl代数，并使用$S$ -合流性质，我们表明，对合集诱导合流重写系统的有理Weyl代数。
2020-07-07 cs.LO
A Note on a Unifying Proof of the Undecidability of Several Diagrammatic Properties of Term Rewriting Systems
本文对项重写系统的几个图形性质的不可判定性给出了一个简单的统一证明，这些性质包括：局部合流性、强合流性、菱形性、次交换性和后继项的存在性。其思想是将图灵机的配置编码为项，然后在这些项上定义一个合适的关系，使得图灵机的终止性等价于图形属性的可满足性。
2019-10-21 cs.LO
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。
2025-10-14 cs.LO
Non-Termination of Logic Programs Using Patterns
univ-reunion（留尼汪大学）
本文提出了一种基于模式的逻辑程序非终止性检测方法，通过新展开技术生成无限集合的有限重写序列，并通过实验验证其有效性。
2026-08-10 cs.LO
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
终止性是程序的一个重要属性，特别是在证明助手中形成的程序。它是项重写系统的图灵完备形式主义中一个非常活跃的研究课题，多年来已经开发了许多方法和工具来解决这个问题。因此，确保这些工具的可靠性是一个重要问题。在本文中，我们提出了一个图书馆正式的重要成果的理论，良好的基础（重写）的关系，在证明助手Coq。我们还提出了其应用程序的终止证书的自动化验证，终止工具。
2012-02-29 cs.LO
CeTA - A Tool for Certified Termination Analysis
自2004年第一次终止竞争以来，人们非常感兴趣的是，由终止工具自动生成的证明是否确实正确。终止证明技术的数量的增加以及生成的证明的复杂性的增加（例如，几种技术的组合、穷举标记、树自动机等），进行认证（即，检查这些证明的正确性对于人类来说越来越乏味。因此，人们对终止证明的自动认证感兴趣。这导致了使用证明助手（如Coq和Isabelle）进行认证的一般方法。我们目前的最新发展IsaFoR/CeTA（版本1.03），这是认证CeTA，基于Isabelle/HOL形式化重写IsaFoR。
2012-08-08 cs.LO
Extending Context-Sensitivity in Term Rewriting
我们提出了一个广义版本的上下文敏感性的术语重写的基础上的“禁止模式”的概念。基本想法是，如果要收缩的Redex具有特定形状并出现在特定上下文中，则应禁止重写步骤。这种形状和背景是通过禁止模式来表达的。特别是，我们分析了这种新的方法和常用的上下文敏感性的概念，在长期重写之间的关系，以及从计算的角度来看，重写与禁止模式的可行性。后一种可行性的特点是要求限制重写关系产生改进的终止行为，同时仍然足够强大，以计算有意义的结果。在某些类的重写系统与禁止模式的两种性质的充分准则。
2010-01-25 cs.LO
A rewriting point of view on strategies
本文是对已发表工作的简要贡献报告。它集中在重写社区中遵循的方法，以正式化策略的概念。基于重写的概念，对策略的几种定义进行了回顾和联系：为了抓住策略的高阶性质，将策略定义为重写逻辑或重写演算中的证明项;并且为了恢复顺序路径构建游戏或函数程序中的策略的定义，策略被认为是与进行中的归约（归约序列中的可能的后续步骤）相关联的部分函数。
2013-03-04 cs.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
Modular Complexity Analysis for Term Rewriting
所有目前的调查，以分析衍生复杂性的长期重写系统是基于一个单一的终止方法，可能之前的转换。然而，由于直接标准的权力有限，专门使用直接标准是有问题的。为了克服这一限制，本文介绍了一个模块化的框架，它允许推断（多项式）上界的复杂性，长期重写系统结合不同的标准。由于其基本思想是基于相对重写，我们研究如何矩阵的解释和匹配边界可以使用和扩展相对重写的复杂性，分别。模块化框架被证明比传统的设置更强大。此外，结果已经实施，实验表明，显着的增益功率。
2014-03-29 cs.LO
Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Extended Version)
从程序转换的问题的动机，八个概念之间的同构术语重写系统的定义，分析和分类。这些概念包括全局同构，其中变量和函数符号的重命名对于系统的所有项重写规则都是相同的，局部同构，其中每个规则使用单个重命名，以及组合，其中一个符号集被全局重命名，而另一个符号集被局部重命名。保存语义属性，如可转换性和终止分析不同的同构概念。引入了项重写系统的模板和极大范式的概念，并给出了有效计算它们的算法。配备这些技术，同构的基本决策问题的复杂性进行了分析，并被证明是有效的解决或证明是完整的图同构复杂性类。
2022-11-30 cs.LO
