Proving confluence of higher-order term rewriting systems automatically

自动证明高阶术语重写系统的汇合

• 批准号: 21700017
• 负责人: IWAMI Munehiro
• 金额: $ 2.75万
• 依托单位: Shimane University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21700017/
• 关键词: 項書換えシステム; 高階項書換えシステム; 無限項書換えシステム; 合流性; 強頭部正規化可能性; 強収束性; 生成性; 一般生成性

We studied several rewriting systems for proving confluence of higher-order term rewriting systems automatically. In this project, we showed many term rewriting systems of combinators do not have strong head normalization. Furthermore, we presented procedures for disproving two properties of infinitary term rewriting systems. the strong head normalization and the productivity. The correctness of our procedures is proved. And we implemented our procedures.

我们研究了几个重写系统，用于自动证明高阶术语重写系统的汇合。在这个项目中，我们展示了组合剂的许多术语重写系统没有强大的头部归一化。此外，我们介绍了无限术语重写系统的两种属性的程序。强大的头部归一化和生产力。证明了我们程序的正确性。我们实施了程序。

项目成果

無限項書き換えシステムにおける性質に関する考察

无限项重写系统中属性的考虑

• 发表时间: 2011
• 期刊: 京都大学数理解析研究所講究録
• 作者: 岩見宗弘;青戸等人
• 通讯作者: 青戸等人

左線形かつK-開発閉包な項書換えシステムの合流性に関する考察

左线性和K-展开封闭项重写系统融合的考虑

• 发表时间: 2010
• 期刊: 京都大学数理解析研究所講究録
• 作者: Michael Hoffmann;Jiri Matousek;Yoshio Okamoto;and Philipp Zumstein;岩見宗弘
• 通讯作者: 岩見宗弘

無限項書換えシステムにおける強頭部正規化可能性の反証手続き

反驳无限项重写系统中强头部归一化性的过程

• 发表时间: 2010
• 期刊: 第12回プログラミングおよびプログラミング言語ワークショップ論文集
• 作者: 岩見宗弘;青戸等人
• 通讯作者: 青戸等人

無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証

无限项重写系统中强头正则性和一般生成性的自动证伪

• 发表时间: 2012
• 期刊: コンピュータソフトウェア
• 作者: 岩見宗弘;青戸等人
• 通讯作者: 青戸等人

組合せ子の強収束性

组合子的强收敛性

• 发表时间: 2009
• 期刊: 第8回情報科学技術フォーラム講演論文集
• 作者: Ondrej Bilka;Kevin Buchin;Radoslav Fulek;Masashi Kiyomi;Yoshio Okamoto;Shin-ichi Tanigawa;Csaba D.Toth;岩見宗弘
• 通讯作者: 岩見宗弘