研究課題
基盤研究(C)
プログラムの性質や仕様を記述する帰納的定理の自動証明法として項書き換えシステムに基づく暗黙的帰納法に着目し、その高度化を図った。主な研究成果としては、書き換え帰納法における順序付け不能な等式の取り扱いを改良するとともに、改良書き換え帰納法に基づく定理自動証明システムを構築した。また、帰納的定理自動証明に重要な補題自動生成法については、健全一般化法の一般化を行った。また、反証機能付き書き換え帰納法に対応する健全発散鑑定法を考案し、さらに、異なる複数の補題を独立に導入する書き換え帰納法フレームワークを考案した。複数の自動補題生成法を効率的に適用する戦略を構築した。また、反証機能付き書き換え帰納法の適用可能性に必要な合流性についてその証明法の理論を拡張するとともに、自動証明システムの構築を行った。
すべて 2011 2010 2009 2008 その他
すべて 雑誌論文 (13件) (うち査読あり 6件) 学会発表 (13件) 備考 (2件)
IEICE Transactions on Information and Systems, , Review existence
巻: Vol.E93-D, No.5 ページ: 963-973
10026815249
Proceedings of the 21st International Conference on Rewriting
巻: Vol.6 ページ: 7-16
IEICE Transactions on Information and Systems
巻: Vol.E93-D ページ: 963-973
Trento, Italy, Review existence
巻: LNAI5749 ページ: 117-132
Brasilia, Brazil, Review existence
巻: LNCS5595 ページ: 93-102
コンピュータソフトウェア
巻: Vol.26, No.2 ページ: 76-92
10025982412
巻: Vol.26, No.2 ページ: 41-55
10025982372
コンピュータソフトウェア 26
ページ: 76-92
ページ: 41-55
Bangalore, India, Dagstuhl Seminar Proceedings, Review existence
巻: Vol.08004 ページ: 13-24
Review existence
巻: Vol.2, No.1 ページ: 61-75
Hagenberg, Austria, Review existence
巻: LNCS5117 ページ: 381-391
巻: 200 ページ: 1-15
http://www.nue.riec.tohoku.ac.jp/index-j.html
