類推に基づくLK証明支援システムの開発
スポンサーリンク
概要
- 論文の詳細を見る
本稿では, LKシーケント計算を対象とした効率的一般証明システムの類推を用いた実現手法について考察する.まず類推を, 一度証明を持つことが検証されたシーケントを抽象化して得られたスキーマー(2階述語論理式)を誘導知識としてもつスキーマー誘導型証明として定式化する.類似性判定は, 与えられたシーケント(1階述語論理式)とスキーマーとのマッチング可能性(2階スキーマーマッチング可能性)として定式化できるが, 一般には難しい問題でありその効果的実現が重要な課題である. 本稿ではスキーマ誘導型証明のためのヒューリスティックスを導入した効率的二階スキーママッチングの実現について述べ, ついでそれを基に実現開発中の対話型のLK証明システムの概要について述べる.
- 社団法人電子情報通信学会の論文
- 2001-11-09
著者
関連論文
- ラベル無し順序木のqグラム距離
- 類推機能をもった対話型シークェント計算証明システムの開発(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(一般及び自動推論)
- MRSAとMSSAを分類する決定木の構築
- The Least Generalization for Bounded Width Clauses (テーマ:特集「ウェブデータの知的処理」および一般)
- イベント列からの扇状エピソード抽出 (テーマ:特集「ウェブデータの知的処理」および一般)
- On Subsumption Algorithm for Chordal Clauses (テーマ:特集「シンボルグラウンディング問題」および一般)
- 間違いの認識による演奏習得支援システムの構築(音楽・演奏の認識合成)
- 人間指向型汎用類推証明システムの開発 (計算機科学基礎理論の新展開)
- 閉単調DNF式被覆の抽出 (特集 オントロジー)
- 類推機能をもった対話型シークェント計算証明システムの開発 (計算機科学基礎理論の新展開)
- Pre-Checkingに基づく効率的スキーママッチングアルゴリズム(LAシンポジウム(情報基礎理論ワークショップ)論文小特集)
- 順序節の包摂と一般化について (論理と学習)
- MRSA検査データからの単調DNF式被覆の抽出
- 類推に基づくLK証明支援システムの開発
- Pre-checkingを用いた効率的2階述語マッチングアルゴリズム (計算理論とアルゴリズムの新展開)
- スキーママッチングを用いたLK類推証明システムの開発
- スキーママッチングとその計算量
- スキーママッチングにおける計算の複雑さ (計算モデルとアルゴリズム)
- スキーママッチングの計算の複雑さ
- 決定可能な高階単一化問題に関する研究 (アルゴリズムと計算の理論)
- 単純型付きラムダ計算における証明文法
- [招待論文]一般単一化理論(「21世紀の知識情報科学に向けて」,及び一般)
- 一般単一化理論
- 型付ラムダ計算における証明文法