2003 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(Petri Net to LLP)およびLLPTTPシステム(LLP Technology Theorem Prover)をベースに線形論理の証明探索を高速に行うシステムLL2LLPをの設計およびプロトタイプ開発を行った.
・LL2LLP(Linear Logic to LLP)は,命題古典線形論理の論理式に対して定理証明を行うシステムである.本システムでは,命題古典線形論理の論理式を代表者らの開発した線形論理型言語LLPのプログラムに変換し,LLPコンパイラ処理系を用いてコンパイル/実行することで証明探索を行う.
プロトタイプを作成し,その速度を他の線形論理自動証明システムと比較したところ,LL2LLPと同様の後向き証明探索を用いているlinseq,タブロー法を用いているlinTAPよりもはるかに高速であった.しかし,前向き証明探索を用いているlinresと比較すると,linresで証明できないがLL2LLPで証明できる問題がある一方,逆にlinresで証明できるがLL2LLPで証明できない問題も存在した.
これは,証明探索の戦略が異なることが原因であると考えられるため,当初の予定通り,証明不可能性の検出を含め,複合的な戦略の利用について今後検討を進める.
|
-
[Publications] 田村直之: "LLPTTP:線形論理型言語コンパイラ処理系を用いた定理証明システム"コンピュータソフトウェア. 20・5. 90-96 (2003)
-
[Publications] S.Ohnishi: "Efficient Representation of Discrete Sets for Constraint Programming"Lecture Notes in Computer Science 2833 : Proc.9th Int'l Conf.on Principles and Practice of Constraint Programming. 920-924 (2003)
