Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems
Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems
复制标题
独特范式的自动证明
DOI：
10.1007/978-3-030-29007-8_19
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Takahito Aoto and Yoshihito Toyama
中科院分区：
文献类型：
--
作者：
Hiroaki Naganuma;Diptarama Hendrian;Ryo Yoshinaka;Ayumi Shinohara;Naoki Kobayashi;Takahito Aoto and Yoshihito Toyama
规范形式的概念在各种等价变换中普遍存在。合流性是项重写系统的核心性质之一，它涉及规范型的唯一性。另一个比汇合弱的性质是唯一范式的性质。转换（conversion）。近年来，TRS的自动融合证明引起了人们的关注，一些功能强大的融合工具集成了多种方法（反）证明的CR性质的TRS已经开发出来。相比之下，还没有多少关于自动证明（disprove）该属性的努力。在本文中，我们报告了一个结合了几种方法的证明（反）的性质。我们提出了一个等价的变换TRS保持，以及一些新的标准（反）证明。
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). Recently, automated confluence proof of TRSs has caught attentions; some powerful confluence tools integrating multiple methods for (dis)proving the CR property of TRSs have been developed. In contrast, there have been little efforts on (dis)proving the UNC property automatically yet. In this paper, we report on a UNC prover combining several methods for (dis)proving the UNC property. We present an equivalent transformation of TRSs preserving UNC, as well as some new criteria for (dis)proving UNC.