文章基本信息
- 标题：LLPTTP: 線形論理型言語コンパイラ処理系を用いた定理証明システム
- 本地全文：下载
- 作者：田村 直之 ; 番原 睦則
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2003
- 卷号：20
- 期号：5
- 页码：502-508
- DOI：10.11309/jssst.20.502
- 出版社：Japan Society for Software Science and Technology
- 摘要：
一階述語論理の節形式をPrologプログラムに変換し，Prologコンパイラ処理系を用いて定理証明を行うシステムとしてPTTP (Prolog Technology Theorem Prover)が知られている．本論文では，節形式を線形論理型言語LLPのプログラムに変換し，LLPコンパイラ処理系を用いることで，より効率的な証明探索が可能になることを示す．特に，証明中のリテラルをリソースとして追加することにより，ME (model elimination)処理を高速化している点に特徴がある．
