汎用前向き帰結演算システムEnCalのインタフェースの開発

概要

論文の詳細を見る
我々は、前向き帰結演算に基づいて推論規則の自動生成と検証、知識自動獲得および自動定理発見を支援するために汎用前向き帰結演算システムEnCalの開発を行っている[1]。帰結演算とは、既知の事実や帰結関係といった前提から、推論規則を適用し、新たな帰結関係を導くことである。EnCalは、論理的帰結演算と経験的帰結演算という二つの機能を利用者に提供する。論理的帰結演算とは、ある論理体系Lの公理図式を与えると、Lの論理定理図式を導くものである。経験的帰結演算とは、ある輪理体系Lの論理定理図式と、ある領域固有の公理の集合Pを与えると、Pを前提として、Lに基づいて経験的定理を導くものである。EnCalの利用対象としているのは、知識処理システムの開発者と、知識処理の研究者、論理学者、数学者、法律家、医者などの知識処理の利用者である。これらの利用者は、計算機の扱いに慣れている人から、計算機にほとんど触ったことのない人までいる。また、論理学の知識がある人から、そうでない人までいる。こういった様々な利用者のためにはインタフェースが重要になる。EnCalのインタフェースへの要求には以下のようなものがある。・EnCalを簡単に起動できる。これは、計算機の扱いに慣れていない人は、複雑な操作を敬遠するからである。・論理式の入力の文法ミスを減らすことができる。これは、論理式の入力ではかっこの対応などの文法ミスを起こしやすいからである。・EnCalを利用する時の作業をまとめて行うことができる。これは、エディタやEnCal本体、ぺージャなどをいちいち起動するのは面倒だからである。・論理式を理解しやすい形で表現することができる。これは、専門家でも論理式をそのままの形で理解することは難しいからである。定理の証明過程や集合演算といった出力結果の解析ができる。これは、推論エンジンだけでなく、解析ツールもユーザに提供するためである。自然言語に近い形で論理式を処理する。これは、ユーザの論理式の入力、理解を支援するためである。
一般社団法人情報処理学会の論文
1997-09-24

汎用前向き帰結演算システムEnCalのインタフェースの開発

スポンサーリンク

概要

著者

関連論文

スポンサーリンク