研究課題
基盤研究(C)
書き換えシステムに基づく帰納的定理の自動証明における補題生成法について、補題候補の発見法や補題決定に有効な技術に資する成果を得た。主な研究成果としては、発散を生じる等式を解析するための基礎理論として、正則項の単一化および書き換え理論、半単一化についての理論について新しい知見を与えた。補題の決定手続きに適した書き換え帰納法の決定理論を拡張するとともに、書き換え帰納法において有効な補題決定手続きについて、始代数を用いるアプローチに基づく新しい手続きを考案した。また、書き換えシステムにおける末尾再帰を用いた関数定義において、自動証明に適した関数定義を得るための補題を抽出する手法を考案した。
すべて 2013 2012 2011 その他
すべて 雑誌論文 (16件) (うち査読あり 16件) 学会発表 (11件) 備考 (1件)
Lecture Notes in Artificial Intelligence
巻: Vol.8152 ページ: 311-326
http://link.springer.com/chapter/10.1007%2F978-3-642-40885-4_22
コンピュータソフトウェア
巻: Vol.30, No.3 ページ: 148-162
Lecture Notes in Computer Science
巻: Vol.7810 ページ: 56-67
http://link.springer.com/chapter/10.1007%2F978-3-642-37064-9_7
巻: Vol.30, No.1 ページ: 187-202
第15回プログラミングおよびプログラミング言語ワークショップ論文集
巻: Vol.7562 ページ: 172-186
http://link.springer.com/chapter/10.1007%2F978-3-642-33654-6_12
Logical Methods in Computer Science
巻: Vol.8, No.1:31 ページ: 1-29
http://www.lmcs-online.org/ojs/viewarticle.php?id=1099&layout=abstract
巻: Vol.29, No.1 ページ: 211-239
巻: Vol.29, No.1 ページ: 176-190
第14回プログラミングおよびプログラミング言語ワークショップ論文集
ページ: 168-182
ページ: 153-167
Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
巻: Vol.10 ページ: 107-121
http://drops.dagstuhl.de/opus/volltexte/2011/3111/
巻: Vol.10 ページ: 91-106
http://drops.dagstuhl.de/opus/volltexte/2011/3110/
第13回プログラミングおよびプログラミング言語ワークショップ論文集
ページ: 99-113
ページ: 84-98
http://www.nue.riec.tohoku.ac.jp/indexj.html