| 研究概要 |
本年度は,線形論理の証明探索を高速に行うシステムのプロトタイプとして,下記の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での特徴であるリソースを用いたプログラミングが有効に働いた結果である。
今後は,開発した上記プロトタイプを元に,線形論理の証明探索システムの開発を進める。また,本年度検討を行った線形論理の証明不可能性の検出アルゴリズムを元に,線形論理の証明不可能性検出システムの開発を進める。
|
