A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
我们引入了一个健全的和完整的共归纳证明系统的可达性的性质在过渡系统中产生的逻辑约束项重写规则的顺序排序签名模内置。微积分的一个关键特征是循环证明规则，它允许获得无限共归纳证明的有限表示。
2018-04-23 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
Complexity Analysis for Call-by-Value Higher-Order Rewriting
本文针对按值调用高阶重写开展研究，提出一种代价-规模语义，通过代数解释将项映射为元组，同时约束归约代价和范式规模，为按值调用程序的建模提供支撑。
2023-07-25 cs.LO
A rewriting point of view on strategies
本文是对已发表工作的简要贡献报告。它集中在重写社区中遵循的方法，以正式化策略的概念。基于重写的概念，对策略的几种定义进行了回顾和联系：为了抓住策略的高阶性质，将策略定义为重写逻辑或重写演算中的证明项;并且为了恢复顺序路径构建游戏或函数程序中的策略的定义，策略被认为是与进行中的归约（归约序列中的可能的后续步骤）相关联的部分函数。
2013-03-04 cs.LO
Rewriting in Free Hypergraph Categories
我们研究重写方程理论的对称monoidal类别的情况下，有一个可分离的Frobenius monoid的每个对象。这些类别，也称为超图类别，越来越相关：弗罗贝纽斯结构最近出现在跨学科应用中，包括量子过程，动力系统和自然语言处理的研究。在这项工作中，我们给出了一个组合特征的箭头的一个自由超图范畴的标记超图的余跨度，并建立一个精确的对应重写模Frobenius结构一方面和双推出重写超图。这种解释允许使用超图上的结果，以确保在一个自由超图类别重写的汇合的可判定性。我们的研究结果概括了以前的方法，其中只考虑由单个对象（道具）生成的类别。
2018-01-03 cs.LO
Termination of rewriting strategies: a generic approach
我们提出了一个通用的终止证明方法重写下的策略，基于一个明确的归纳终止属性。重写树的基础条款的证明树，交替应用缩小和抽象的步骤产生的模型。归纳原理是通过抽象机制来应用的，在抽象机制中，术语被表示其任何范式的变量所替换。归纳排序不是先验给出的，而是用排序约束定义的，在证明过程中递增设置。抽象约束可以用来控制收缩机制，众所周知，收缩机制很容易发散。然后为最内层、最外层和局部策略实例化泛型方法。
2005-07-26 cs.LO
Rewriting and Inductive Reasoning
针对传统重写在归纳推理中遗漏关键后承的问题，本文扩展 superposition 演算以在饱和中自动生成充分后承，并在 Vampire 上验证其单元等式归纳推理性能显著提升。
2024-02-29 cs.LO
Templates in Rewriting Induction
Radboud University, Nijmegen（奈梅亨拉德堡德大学）
本文提出基于模板的重写归纳方法，用于生成归纳假设，以分析实际编程代码，弥补传统方法在处理约束和计算时的不足。
2026-07-23 cs.LO
Sound, Complete and Minimal UCQ-Rewriting for Existential Rules
University Montpellier 2（蒙彼利埃第二大学）；TU Dresden（德累斯顿工业大学）
我们解决基于本体的数据访问的问题，与本体表示的存在规则的框架，也被称为数据库+/-。一种公知的方法涉及使用本体知识重写查询。在这里，我们专注于基本的重写技术，其中包括重写成一个联盟的合取查询的初始查询。首先，我们研究了一个通用的宽度优先重写算法，它需要作为输入的任何重写操作，并定义属性的重写操作，以确保算法的正确性。然后，我们专注于片统一，它提供了一个重写操作所需的属性。最后，我们提出了这个框架的实现，并报告了一些实验。
2013-11-13 cs.AI cs.LO
Definitions by rewriting in the Calculus of Constructions
本文提出了一般的语法条件，确保强规范化和逻辑一致性的演算代数构造，一个扩展的演算构造与功能和谓词定义的高阶重写规则。一方面，构造演算是一个功能强大的类型系统，在其中可以形式化高阶逻辑的命题和自然演绎证明。另一方面，重写是一种简单而强大的计算范式。两者的结合允许，除其他事项外，开发正式的证明与更传统的证明助手相比，具有更小的尺寸和更多的自动化。主要的新颖之处是考虑重写的一般形式，在谓词级，概括了强消除的演算归纳结构。
2006-10-12 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
Verifying Procedural Programs via Constrained Rewriting Induction
本文提出将过程式程序转换为逻辑约束项重写系统，通过扩展重写归纳方法自动验证内存安全性和函数正确性，并证明实现间等价性，无需单独规范语言。
2025-08-29 cs.LO
Compositional specification in rewriting logic
重写逻辑自然是并发的：状态项的几个子项可以同时重写。但是状态术语是全局的，这使得组合性很难实现。这里的组合性意味着能够将复杂的系统分解成其功能组件，并将每个组件作为一个隔离和封装的系统进行编码。我们的目标是帮助在重写逻辑时将组合性引入系统规范。我们建议的基础是我们称之为同步合成的操作。我们讨论的动机和影响，我们的建议，形式化的重写逻辑和过渡结构，作为语义，并显示我们的方法与一些例子的力量。这篇论文是在逻辑程序设计理论与实践（TPLP）中考虑的。
2020-01-30 cs.LO
Modes of Convergence for Term Graph Rewriting
项图重写提供了一种简单的机制来表示受限形式的无穷项重写。无穷项重写与项图重写之间的对应关系已经得到了一定程度的研究。然而，这一努力是削弱了缺乏一个适当的对应的无限重写的一方的长期图。我们的目标是填补这一空白，设计了两种模式的收敛的基础上分别为一个度量的偏序图。由此获得的结构概括了相应的模式的收敛，通常是在无穷项重写研究。我们认为，这产生了一个共同的框架，在其中长期重写和长期图重写可以研究。为了证实我们的主张，我们比较了术语图和术语上的收敛性。特别是，我们表明，长期图上的收敛模式是保守的扩展，相应的模式收敛的条款，并保存unravelling长期图的条款。此外，我们发现，许多已知的无穷项重写的属性被保留。这包括两种收敛模式的内在完备性，以及通过偏序收敛是度量收敛的保守扩展。
2012-05-31 cs.LO cs.PL
Lynch-Morawska Systems on Strings
我们研究收敛和前向封闭的字符串重写系统的语法标准的上下文中介绍的\cite{LynchMorawska}由克里斯托弗林奇和芭芭拉Morawska（我们称之为$LM$ -系统）。由于一个字符串重写系统可以被看作是一个术语重写系统的签名的纯一元函数符号，我们适应他们的定义字符串重写的情况。我们证明了收敛的前向闭弦重写系统的子项崩溃问题是有效可解的。因此，存在一种判定过程，该判定过程验证这样的系统是否是$LM$系统。我们使用相同的结构证明了\emph{cap problem}从该领域的密码协议分析，这是不可判定的一般$LM$ -系统，是可判定时，限制到字符串重写的情况下。
2016-06-01 cs.LO
Number representations and term rewriting
在本文中，我们研究了一些整数表示的项重写系统，进一步建立在[2]中描述的数据类型定义系统的基础上。特别是，我们看看自动化的方法证明合流和终止在二进制和十进制项重写系统的追加和树构造函数。我们发现，这些长期重写系统中的一些不强烈终止，我们解决这些系统的微小变化。此外，大多数讨论的术语重写系统不表现出合流性质，这似乎更难以解决。
2016-07-15 cs.DS cs.LO
Hypergraph rewriting and Causal structure of $λ-$calculus
该研究从范畴论角度研究超图重写以定义事件并构建图重写因果基础，还研究λ演算中事件的因果判定算法并尝试将其扩展到任意λ表达式。
2024-11-02 cs.DM cs.LO
Linear Compressed Pattern Matching for Polynomial Rewriting (Extended Abstract)
本文是一个扩展的抽象分析的长期重写的重写规则中的条款，以及长期重写压缩的单例树文法（STG）。这种形式的压缩比节点共享或将项表示为dag更一般，因为部分树（上下文）也可以在压缩中共享。在第一部分中，高效，但复杂的算法检测适用性的重写规则下STG压缩构造和分析。第二部分将这些结果应用于项重写序列。子匹配的主要结果是，找到一个左线性规则的redex可以在多项式时间STG压缩下执行。重写和（单位置或并行）重写步骤的主要含义是：（i）在STG压缩下，n个重写步骤可以在非确定性多项式时间内执行。(ii)在STG压缩下，对于左线性重写规则，可以在多项式时间内执行n个重写步骤的序列，以及（iii）对于压缩重写规则，其中左手侧或者是DAG压缩的，或者是地面和STG压缩的，以及STG压缩的目标项，可以在多项式时间内执行n个重写步骤。
2013-02-26 cs.DS cs.LO
Partial Order Infinitary Term Rewriting
我们研究了无穷项重写的另一种模型。而不是一个度量的条款，偏序部分条款的形式化收敛的减少。我们认为，一个弱的和强的收敛性的概念，并表明，度量模型的收敛性与偏序模型限制总条款。因此，偏序收敛构成了度量收敛的保守扩展，它还提供了不同水平的发散之间的细粒度区分。第二部分主要研究正交系的强收敛性。主要结果是，度量模型和偏序模型之间的差距可以通过扩展的条款重写系统的额外规则来弥合。这些扩展是著名的Böhm扩展。基于这一结果，我们能够建立-相反的度量设置-正交系统都是无限合流和无限规范化的偏序设置。偏序模型所允许的唯一无穷范式是Böhm树。
2014-06-02 cs.LO
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
本文针对概率项重写系统的 iAST 问题，重新定义依赖对并引入新转换，将不完备的依赖元组方法发展为完备的概率 DP 框架，且在 AProVE 中验证其证明能力显著提升。
2024-02-29 cs.LO
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
本文提出一个基于等式谓词、上下文重写和变体化简的归纳推理系统，20条规则中仅9条需用户交互，其余11条可自动执行，大部分已在Maude的NuITP中实现。
2024-05-03 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
A term-rewriting characterization of PSPACE
Isabel Oitavem介绍了一个术语重写系统（TRS），它捕获了多项式空间可计算函数的FPS类。我们提出了一种替代TRS FPS。由此得到FPS是包含某些初始函数的最小类，且在特定运算下是闭的。事实证明，我们的特征是相对简单的，并建议一个统一的方法的空间复杂性。
2012-01-03 cs.LO math.LO
Generic Encodings of Constructor Rewriting Systems
Université de Lorraine（洛林大学）；LORIA（洛林计算机科学及其应用实验室）
重写是一种广泛应用于计算机科学和数理逻辑的形式主义。经典的形式主义已经扩展，在函数式语言的上下文中，与规则的顺序，并在基于重写的语言的上下文中，与模式的否定。本文提出了一种简洁明了的模式差异计算算法，该算法可用于将具有否定和顺序的构造函数项重写系统的通用编码定义为经典项重写系统。作为一个直接的后果，建立的方法用于长期重写系统可以应用到分析的扩展系统的属性。该方法也可以被看作是一个通用的编译器，其目标是提供基本模式匹配原语的任何语言。形式主义也提供了一个新的方法来决定一组模式是否包含一个给定的模式，从而检查无用模式的存在或模式的完整性。
2019-06-11 cs.CL cs.LO cs.PL
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to \emph{tuples} of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type $\mathsf{nat}$ may be associated to a pair $(\mathsf{cost}, \mathsf{size})$ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexit…
2021-05-03 cs.LO cs.SC
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
Nominal Equational Rewriting and Narrowing
本文首次定义等式理论取模下的标称重写与窄化，建立标称E-一致性并证明标称E-提升定理，为通过标称等式窄化实现正确的标称等式合一算法奠定理论基础。
2025-06-06 cs.LO cs.SC
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
在本文中，我们提出了一种新的方法，一个命令式程序的函数调用和全局变量转换成一个逻辑约束的长期重写系统。所得到的系统用调用堆栈表示整个执行环境的转换。更准确地说，我们为整个环境准备了一个函数符号，它存储全局变量的值和一个调用堆栈作为其参数。对于一个函数调用，我们准备重写规则来将帧压入堆栈，并在执行后弹出它。任何运行的框架都位于堆栈的顶部，访问全局变量的语句由环境符号的重写规则表示。我们展示了一个精确的转换的基础上的方法，并证明其正确性。
2019-02-22 cs.LO cs.PL
Monads, partial evaluations, and rewriting
单子可以被解释为编码形式表达式，或泛代数意义上的形式运算。我们给出了一个构造，它形式化了“部分求值表达式”的概念：例如，“2+3”可以作为“2+2+1”的部分求值来获得。这个构造可以对任何单子给出，并且它与著名的bar构造有关，它给出了一个运算解释：bar构造诱导一个单纯集，它的1-胞是部分求值。研究了一般单子的部分求值的性质。我们证明了，只要单子是弱carnival，部分评价可以组成通过通常的Kan填充属性的单纯集，其中我们给出了一个解释的条款替换。在重写方面，部分评价给出了一个抽象的约简系统，它是自反的，融合的，传递的，只要单子是弱carnival的。对于概率单子的情况，部分评估对应于概率学家所说的随机变量的条件期望。这份手稿是正在进行的工作的一部分，对酒吧建设的一般重写解释。
2020-05-17 cs.LO math.CT
