| 配分額 *注記 |
4,000千円 (直接経費: 4,000千円)
2004年度: 1,300千円 (直接経費: 1,300千円)
2003年度: 1,300千円 (直接経費: 1,300千円)
2002年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| 研究概要 |
平成14〜16年度において,以下のように線形論理の自動演繹システムについて,ソフトウェア開発および研究発表を行った.
・LLPTTP(LLP Technology Theorem Prover)の設計と開発
LLPTTPは,古典論理の節形式に対して定理証明を行うシステムである(雑誌論文-1).本システムでは,節形式を線形論理型言語LLPのプログラムに変換し,LLPコンパイラ処理系を用いてコンパイル/実行することで定理証明を行っている.
LLPTTPシステムの性能を,TPTP問題セットに対して,既存のPTTP(Prolog Technology Theorem Prover)およびlolliCoPと比較した結果,より良い結果を得られることが確認できた.
・LL2LLP(Linear Logic to LLP)の設計と開発
LL2LLPは,命題古典線形論理の論理式に対して定理証明を行うシステムである(雑誌論文-2,6).本システムでは,命題古典線形論理の論理式を代表者らの開発した線形論理型言語LLPのプログラムに変換し,LLPコンパイラ処理系を用いてコンパイル/実行することで証明探索を行う.
証明探索の性能を,linres, linseq, linTAP等の他の線形論理自動証明システムと比較したところ,多くの問題についてはるかに効率良い証明探索が行えることが確認できた.
・検証システムへの応用
慶應大学の岡田教授らと,実時間システムの仕様記述検証に関する共同研究を行い,線形論理を用いた検証システムのプロトタイプを開発し,その成果について国際ワークショップでデモンストレーションを含めた研究発表を行った(雑誌論文-4,5).
|
