2002 Fiscal Year Annual Research Report
| Project/Area Number |
14580375
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, 工学部, 助教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 奈良工業高等専門学校, 一般教科, 講師 (80290774)
|
|---|
| Keywords | 線形論理 / 自動演繹 / 自動証明 / 定理証明 |
|---|
| Research Abstract |
本年度は,線形論理の証明探索を高速に行うシステムのプロトタイプとして,下記のPN2LLPおよびLLPTTPシステムを開発し,線形論理の証明不可能性の検出アルゴリズムについて検討を行った.
・PN2LLP(Petri Net to LLP)は,線形論理の論理式のうちペトリネットに対応する論理式の証明可能性を解析することで,元のペトリネットの到達可能性を解析するシステムである([雑誌論文]-1で発表)。本システムでは,ペトリネットに対応した線形論理の論理式を,代表者らの開発した線形論理型言語LLPのプログラムに変換し,LLPコンパイラ処理系を用いてコンパイル/実行することで到達可能性を判定している。
・LLPTTP(LLP Technology Theorem Prover)は,古典論理の節形式に対して定理証明を行うシステムである([雑誌論文]-2で発表)。本システムでは,節形式を線形論理型言語LLPのプログラムに変換し,LLPコンパイラ処理系を用いてコンパイル/実行することで定理証明を行っている。
LLPTTPシステムの性能を,TPTP問題セットに対して,既存のPTTP(Prolog Technology Theorem Prover)およびlolliCoPと比較した結果,より良い結果を得られることが確認できた。これは,線形論理型言語LLPでの特徴であるリソースを用いたプログラミングが有効に働いた結果である。
今後は,開発した上記プロトタイプを元に,線形論理の証明探索システムの開発を進める。また,本年度検討を行った線形論理の証明不可能性の検出アルゴリズムを元に,線形論理の証明不可能性検出システムの開発を進める。
|
Research Products
(4 results)
-
[Publications] M.Banbara, T.Tanizawa, N.Tamura: "Demonstration of Compiler Systems for Linear Logic Programming Languages and their Applications"Workshop on Logic and Computation with the Special Intensive Lecture Series by J-Y. Girard. (口頭発表). (2003)
-
[Publications] 田村直之, 番原睦則: "LLPTTP:線形論理型言語コンパイラ処理系を用いた定理証明システム"日本ソフトウェア科学会第19回大会講演論文集. 7A-4 (2002)
-
[Publications] 田村直之: "[特別招待論文]線形論理と論理プログラミング"電子情報通信学会技術研究報告. 102・91. 37-42 (2002)
-
[Publications] M.Banbara: "Design and Implementation of Linear Logic Programming Languages"神戸大学大学院自然科学研究科 学位論文. 97 (2002)
