Proving confluence of higher-order term rewriting systems automatically
Proving confluence of higher-order term rewriting systems automatically
自动证明高阶术语重写系统的汇合
批准号：
21700017
负责人：
IWAMI Munehiro
金额：
$2.75万
依托单位：
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2009
资助国家：
日本
项目状态：
已结题
起止时间：
2009 至 2011
中文摘要
翻译
研究了几种用于自动证明高阶项重写系统合流性的重写系统。在这个项目中，我们证明了许多组合子的项重写系统不具有强头部规范化。此外，我们还给出了证明无穷项重写系统的两个性质的方法。强头规范化和生产力。我们的程序的正确性得到了证明。我们执行了我们的程序。
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
無限項書き換えシステムにおける性質に関する考察
无限项重写系统中属性的考虑
无限项重写系统中属性的考虑
DOI：
--
发表时间：
2011
期刊：
京都大学数理解析研究所講究録
影响因子：
--
作者：
[岩見宗弘, 青戸等人]
通讯作者：
青戸等人
左線形かつK-開発閉包な項書換えシステムの合流性に関する考察
左线性和K-展开封闭项重写系统融合的考虑
左线性和K-展开封闭项重写系统融合的考虑
DOI：
--
发表时间：
2010
期刊：
京都大学数理解析研究所講究録
影响因子：
--
作者：
[Michael Hoffmann, Jiri Matousek, Yoshio Okamoto, and Philipp Zumstein, 岩見宗弘]
通讯作者：
岩見宗弘
無限項書換えシステムにおける強頭部正規化可能性の反証手続き
反驳无限项重写系统中强头部归一化性的过程
反驳无限项重写系统中强头部归一化性的过程
DOI：
--
发表时间：
2010
期刊：
第12回プログラミングおよびプログラミング言語ワークショップ論文集
影响因子：
--
作者：
[岩見宗弘, 青戸等人]
通讯作者：
青戸等人
組合せ子の強収束性
组合子的强收敛性
组合子的强收敛性
DOI：
--
发表时间：
2009
期刊：
第8回情報科学技術フォーラム講演論文集
影响因子：
--
作者：
[Ondrej Bilka, Kevin Buchin, Radoslav Fulek, Masashi Kiyomi, Yoshio Okamoto, Shin-ichi Tanigawa, Csaba D.Toth, 岩見宗弘]
通讯作者：
岩見宗弘
無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証
无限项重写系统中强头正则性和一般生成性的自动证伪
无限项重写系统中强头正则性和一般生成性的自动证伪
DOI：
--
发表时间：
2012
期刊：
コンピュータソフトウェア
影响因子：
--
作者：
[岩見宗弘, 青戸等人]
通讯作者：
青戸等人