• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

1993 Fiscal Year Annual Research Report

高速推論を目的とする一階論理コンパイラに関する研究

Research Project

Project/Area Number 05780238
Research InstitutionUniversity of Yamanashi

Principal Investigator

岩沼 宏治  山梨大学, 工学部, 助教授 (30176557)

Keywords一階論理 / モデル消去法 / 自動証明 / 定理証明 / Prolog / コンパイラ / 補題
Research Abstract

本研究では、一階論理の高速推論を目的として、一階論理式を機械語プログラム翻訳し計算機上で直接実行させるための、一階論理コンパイラの研究・開発を行った。
本コンパイラは証明すべき一階式が与えられたとき、まずその上の順序付線形導出法を模倣するPrologプログラムを生成する。次に証明中で生成される冗長な節や恒真節の消去を目的とした枝刈コードの挿入など幾つかの最適化処理を行い、最終的にPrologコンパイラを用いて機械語プログラムへ変換する。実験により、初期の目的であった1桁以上の高速化が達成されたことを確認している。
また本研究では補題(1emma)処理に関しても研究を行った。既在の研究により、補題の導入は重複計算の抑制に非常に有効であることが示されているが、逆に探索空間の増大をもたらす欠点の知られている。本研究では、不必要な探索空間の増大を抑制する目的として、現代的なPrologシステムに備わっている遅延演算子を利用した実行メカニズムを開発した。これは変数代入を極力抑制し、複数の探索パスを統合化(一本化)することにより、探索空間の縮小を図るものである。実験により、かなりの効果があることを確認している。

  • Research Products

    (2 results)

All Other

All Publications (2 results)

  • [Publications] 芦澤.芳野.三橋.岩沼: "一階理論コンパイラ作成に向けての予備実験について" 電子情報通信学会.技術研究報告. AI23-93. 41-48 (1993)

  • [Publications] 岩沼 宏治: "PTTPに基づくサーカムスクリプションのコンパイル方法" 情報処理学会.「知識のリフォメーションシンポジウム」論文集. 1-10 (1993)

URL: 

Published: 1995-05-17   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi