Research on automated confluence proving for term rewriting systems

术语重写系统自动汇合证明研究

• 批准号: 22500002
• 负责人: TOYAMA Yoshihito
• 金额: $ 2.33万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22500002/
• 关键词: 書き換えシステム; 合流性; 自動検証; 停止性; モジュラ性

The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although many automated termination provers of term rewriting systems have been proposed recently, little work is reported on automated confluence provers. This research aims to develop an automated confluence prover ACP for term rewriting systems based on several methods. Concrete results include a reduction-preserving completion method for proving confluence, one side decreasing diagram method for proving commutativity, a path ordering for guaranteeing polynomial size normal forms, a confluence proof method based on persistency. In the first confluence competition for term rewriting systems (IWC 2012), ACP developed by our group has won first place among the three participants.

术语重写系统理论广泛应用于自动定理证明和计算模型领域。虽然许多自动终止证明的长期重写系统已被提出最近，很少有工作报告的自动合流证明。本研究旨在发展一个自动汇流证明器ACP的术语重写系统的基础上的几种方法。具体成果包括证明合流性的保持归约的完备化方法、证明可交换性的一侧递减图方法、保证多项式大小范式的路径排序、基于持续性的合流性证明方法。在第一届术语重写系统汇流竞赛（IWC 2012）中，我们开发的ACP在三个参赛者中获得了第一名。

项目成果

A reduction-preserving completion for proving confluence of non-terminating term rewriting systems

证明非终止术语重写系统汇合的保留归约完成

• 发表时间: 2012
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Kazuhide Nishikawa;Takao Nishizeki and Xiao Zhou;Hayashi M;Jesmin S;Takahito Aoto and Yoshihito Toyama
• 通讯作者: Takahito Aoto and Yoshihito Toyama

Automated confluence proof by decreasingdiagrams based on rule-labelling

基于规则标签的递减图自动汇合证明

• 发表时间: 2010
• 作者: Takahito Aoto ;Yoshihito Toyama;M. Kano and M. Uno;桃井達明,須鎗弘樹;飯田沙緒里,須鎗弘樹;Takahito Aoto
• 通讯作者: Takahito Aoto

Reduction-preserving completion for proving confluence of non-terminating term rewriting systems

用于证明非终止项重写系统汇合的约简保持完成

• 发表时间: 2011
• 期刊: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
• 作者: Takahito Aoto;Yoshihito Toyama
• 通讯作者: Yoshihito Toyama

多項式サイズ正規形を保証する項書き換えシステムの経路順序

保证多项式大小范式的项重写系统的路径排序

• 发表时间: 2012
• 期刊: コンピュータソフトウェア
• 作者: 磯部耕己;青戸等人;外山芳人
• 通讯作者: 外山芳人

Termination of rule-based calculi for uniform semi-unification

均匀半统一的基于规则的计算的终止

• 发表时间: 2013
• 作者: T. Ito;T. Nishizeki;M. Schroder;T. Uno;X. Zhou;阿部 達也;古賀弘樹，児矢野和也;Takahito Aoto and Munehiro Iwami
• 通讯作者: Takahito Aoto and Munehiro Iwami