文章基本信息
- 标题：線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム
- 本地全文：下载
- 作者：田村 直之 ; 番原 睦則
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2005
- 卷号：22
- 期号：1
- 页码：1_98-1_103
- DOI：10.11309/jssst.22.1_98
- 出版社：Japan Society for Software Science and Technology
- 摘要：
本論文では，著者らの開発した線形論理型言語コンパイラ処理系のLLPを用いて，古典命題線形論理の論理式の証明探索を行うシステムLL2LLPについて述べる．本システムは，古典命題線形論理式を直観主義線形論理式に変換し，さらにLLPコンパイラを用いてLLP抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現している点に特徴がある．いくつかの線形論理式に対して，既存の線形論理定理証明システムと性能を比較した所，ほとんどの問題でより良い結果が得られた．
