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.

术语重写系统的理论被广泛用于自动定理证明和计算模型的领域。尽管最近提出了许多术语重写系统的自动终止差异，但对自动化汇合剂掠夺的报道很少。这项研究旨在开发一种基于几种方法的术语重写系统的自动化汇合供prover 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

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

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

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

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

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