| 研究概要 |
本年度は,昨年度開発した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で証明できない問題も存在した.
これは,証明探索の戦略が異なることが原因であると考えられるため,当初の予定通り,証明不可能性の検出を含め,複合的な戦略の利用について今後検討を進める.
|
