Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs

抽象归约系统合流性证明的新方法——非E-重叠弱浅层项重写系统的合流性——

A new method for proving confluence on abstract reduction systems --- Confluence of non-E-overlapping weakly-shallow TRSs ---

本文提出一种通过相容性和边交换性条件扩展有限子ARS来证明合流性的新方法，并应用于证明非E-重叠弱浅层TRS的合流性，去掉了非坍缩假设，得到可判定的合流充分条件。

Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems

The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness of normal forms. Yet another such property, which is weaker than confluence, is the property of unique normal forms w.r.t. conversion (UNC). Famous examples having UNC but not CR include the TRSs consisting of S,K,I-rules for the combinatory logic supplemented with various pairing rules (de Vrijer, 1999). Recently, automated confluence proof of TRSs has caught attentions leading to investigations of automatable meth…

正交重写系统汇流的形式化

Formalizing the Confluence of Orthogonal Rewriting Systems

可确定性是一种编程原则，它以语法的方式保证功能规范的确定性。基本上，正交性一方面避免了非确定性的固有模糊性，禁止存在指定相同函数的不同规则并且可以同时应用（非模糊性），另一方面，它消除了在这些规则的左侧出现变量重复的可能性（左线性）。在术语重写系统（TRS）理论中，确定性被众所周知的汇合性质所捕获，该性质基本上表明，无论何时从一个术语进行不同的计算或简化都是可能的，计算出的答案应该一致。虽然证明在技术上是详尽的，但汇流是众所周知的正交性的结果。因此，正交性是递归函数的规范所固有的一个重要的数学学科，它自然地应用于函数式编程和规范。从形式化的理论TRS的证明助手PVS，这项工作描述了如何融合的正交TRS已正式化，公理化的基础上的属性的规则，位置和替代参与并行步骤的减少，在这个证明助手。证明了一些类似的，但限制性的性质，如非二义性和（左和右）线性TRS的合流的性质已经完全形式化。

递减图汇流--形式化

Confluence by Decreasing Diagrams -- Formalized

本文给出了定理证明器Isabelle中递减图的形式化。它讨论了机械证明，表明任何局部减少的抽象重写系统是合流。考虑了谷值和递减图的转换形式。