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回プログラミングおよびプログラミング言語ワークショップ論文集
• 作者: 岩見宗弘;青戸等人
• 通讯作者: 青戸等人

組合せ子の強収束性

组合子的强收敛性

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

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

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

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