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
Termination of rewriting strategies: a generic approach
我们提出了一个通用的终止证明方法重写下的策略，基于一个明确的归纳终止属性。重写树的基础条款的证明树，交替应用缩小和抽象的步骤产生的模型。归纳原理是通过抽象机制来应用的，在抽象机制中，术语被表示其任何范式的变量所替换。归纳排序不是先验给出的，而是用排序约束定义的，在证明过程中递增设置。抽象约束可以用来控制收缩机制，众所周知，收缩机制很容易发散。然后为最内层、最外层和局部策略实例化泛型方法。
2005-07-26 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
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
Extending Context-Sensitivity in Term Rewriting
我们提出了一个广义版本的上下文敏感性的术语重写的基础上的“禁止模式”的概念。基本想法是，如果要收缩的Redex具有特定形状并出现在特定上下文中，则应禁止重写步骤。这种形状和背景是通过禁止模式来表达的。特别是，我们分析了这种新的方法和常用的上下文敏感性的概念，在长期重写之间的关系，以及从计算的角度来看，重写与禁止模式的可行性。后一种可行性的特点是要求限制重写关系产生改进的终止行为，同时仍然足够强大，以计算有意义的结果。在某些类的重写系统与禁止模式的两种性质的充分准则。
2010-01-25 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
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
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
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
Star Games and Hydras
本文通过引入星游戏简化递归路径排序的表述，并直接证明了九头蛇战役的终止性，同时提供了量化版本及未来研究方向。
2021-05-26 cs.LO
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
2019-04-04 cs.LO cs.PL
Automated verification of termination certificates
为了增加用户的信心，许多自动定理证明器提供可以独立验证的证书。在本文中，我们报告了我们的进展，在开发一个独立的工具，用于检查证书的正确性终止长期重写系统，并正式证明其正确性的证明助手Coq。为此，我们使用Coq的提取机制和库上的重写理论和终止称为CoLoR。
2012-12-11 cs.LO cs.MS cs.SE
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
Argument filterings and usable rules in higher-order rewrite systems
静态依赖对方法是一种证明高阶重写系统可终止性的方法。它结合了一阶重写系统中引入的依赖对方法和类型化可重写演算中引入的强可计算性概念。参数过滤和可用规则是当前一阶自动终止证明器使用的依赖对框架的两个重要方法。在本文中，我们扩展了一类高阶系统上的静态依赖对方法可以应用。然后，我们扩展参数过滤和可用的规则，高阶重写，从而提供了一个强大的自动终止证明高阶重写系统的基础。
2011-09-20 cs.LO
Local Termination: theory and practice
终止使用良好的基础单调代数的表征是自动终止技术的一个里程碑，在过去的几年里，我们已经看到了广泛的发展。术语重写系统（TRS）的语义特征和大多数已知的终止方法都涉及全局终止，即所有术语的一致终止。在本文中，我们考虑本地终止，在一个给定的TRS的特定条款集。本文的主要目标是概括的语义特征的整体终止本地终止。这是可能的，通过承认良基单调代数是部分的。我们还将我们的方法扩展到本地相对终止。对局部终止的兴趣自然出现在程序验证中，在那里人们可能只对合理的输入感兴趣，或者只是想验证程序终止的输入集。当处理TRS中已知为非终止的特定类别的术语时，局部终止也将是感兴趣的，例如组合逻辑（CL）或TRS编码递归程序方案或图灵机。我们展示了如何证明全球终止的一些著名的技术，如逐步删除重写规则和语义标签，可以适应当地的情况。我们还描述了减少局部到全局终止问题的转换。由此产生的证明本地终止的技术在某些情况下已经自动化。我们的应用之一涉及CL作为正则语言的终止S-项的特征。在此之前，这种语言已经通过对S项的归约行为进行繁琐的分析而被发现。这些发现现在已经被一个完全自动化和经过验证的证明所证实。
2010-09-07 cs.LO
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems
高阶重写系统（HRS）和简单类型项重写系统（STRS）是函数式程序的计算模型。我们最近提出了一个非常强大的方法，静态依赖对方法，这是基于强可计算性的概念，以证明终止STRS。在本文中，我们将该方法扩展到HRSs。由于HRSs包含λ-抽象而STRSs不包含λ-抽象，我们重新构造了静态依赖对方法以允许λ-抽象，并表明静态依赖对方法在没有新限制的情况下也能很好地工作在HRSs上。
2011-09-26 cs.LO
