線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム Classical Propositional Linear Logic Theorem Prover on a Linear Logic Programming Language Compiler System

この論文をさがす

著者

抄録

本論文では,著者らの開発した線形論理型言語コンパイラ処理系のLLPを用いて,古典命題線形論理の論理式の証明探索を行うシステムLL2LLPについて述べる.本システムは,古典命題線形論理式を直観主義線形論理式に変換し,さらにLLPコンパイラを用いてLLP抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現している点に特徴がある.いくつかの線形論理式に対して,既存の線形論理定理証明システムと性能を比較した所,ほとんどの問題でより良い結果が得られた.his paper describes a theorem prover of propositional classical linear logic implemented on a linear logic programming language developed by the authors. In this LL2LLP system, efficient proof search is realized by transforming classical linear logic formulas into intuitionistic linear logic formulas, and by compiling them into LLP abstract machine instructions. The evaluated performance of LL2LLP was better than other existing provers for most of the benchmark problems.

This paper describes a theorem prover of propositional classical linear logic implemented on a linear logic programming language developed by the authors. In this LL2LLP system, efficient proof search is realized by transforming classical linear logic formulas into intuitionistic linear logic formulas, and by compiling them into LLP abstract machine instructions. The evaluated performance of LL2LLP was better than other existing provers for most of the benchmark problems.

収録刊行物

  • コンピュータソフトウェア = Computer software

    コンピュータソフトウェア = Computer software 22(1), 98-103, 2005-01-26

    Japan Society for Software Science and Technology

参考文献:  23件中 1-23件 を表示

被引用文献:  1件中 1-1件 を表示

各種コード

  • NII論文ID(NAID)
    110003744168
  • NII書誌ID(NCID)
    AN10075819
  • 本文言語コード
    JPN
  • 資料種別
    Journal Article
  • ISSN
    02896540
  • NDL 記事登録ID
    7235970
  • NDL 雑誌分類
    ZM13(科学技術--科学技術一般--データ処理・計算機)
  • NDL 請求記号
    Z14-1033
  • データ提供元
    CJP書誌  CJP引用  NDL  NII-ELS  IR  J-STAGE 
ページトップへ