2004 Fiscal Year Annual Research Report
| Project/Area Number |
14580375
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, 学術情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 神戸大学, 学術情報基盤センター, 講師 (80290774)
|
|---|
| Keywords | 線形論理 / 自動演繹 / 自動証明 / 定理証明 |
|---|
| Research Abstract |
本年度は,以下の研究成果を得た.
・線形論理の定理証明システムLL2LLPの改良
LL2LLP(Linear Logic to LLP)は,命題古典線形論理の論理式に対して定理証明を行うシステムである.昨年度のプロトタイプを改良し,既存の線形論理定理証明システムよりはるかに高速に定理証明を行えることを確認し,その成果をまとめ研究発表を行った.また,LL2LLPのベースとなっている線形論理型言語のコンパイラ処理系LLPに関しても,日本学術振興会外国人特別研究員のJ.Polakow氏らと,より効率の良い計算モデルに関する研究を行った.
・検証システムへの応用
慶應大学の岡田教授らと,実時間システムの仕様記述検証に関する共同研究を行い,線形論理を用いた検証システムのプロトタイプを開発し,その成果について国際セミナーで研究発表とデモンストレーションを行った.
|
