非再帰的な述語サーカムスクリプションの一階論理式への等価変換
スポンサーリンク
概要
- 論文の詳細を見る
In this paper, we present a method which transforms predicate circumscription into a first-order sentence if its condition sentence is non-recursive with respect to predicates to be minimized. So far, fundamentally, the concept of the recursion in aribitrary first-order formulas has not been so clear. Therefore, at first, we consider and formalize this concept. Next, we define a computational condition that a formula is non-recursive with respect to predicates, and give an equivalent transformation method of non-recursive predicate circumscription into first-order sentences. A non-recursive formula A with respect to predicates p_1,…,p_n is defined only by the relations between positive and negative occurrences of p_1,…,p_n in A, without considering the number of the occurrences or the kinds of the quantification. Therefore, this transfomation method can deal with complex predicate circumscription such that its condition sentence is non-definite with respect to minimized predicates, or is quantified with both existential and universal quantifiers in any forms.
- 1990-07-01
著者
関連論文
- ラベル無し順序木のqグラム距離
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(1997-2001)
- 類推機能をもった対話型シークェント計算証明システムの開発(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(一般及び自動推論)
- 投機的計算によるSATプランニングの効率改善に関する研究(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- 超高速ATM LANの構築法と次世代ユーザーインタフェースに関する研究
- 4. 抽象化に基づく類推 (<特集> アナロジー)
- 間違いの認識による演奏習得支援システムの構築(音楽・演奏の認識合成)
- 人間指向型汎用類推証明システムの開発 (計算機科学基礎理論の新展開)
- 類推機能をもった対話型シークェント計算証明システムの開発 (計算機科学基礎理論の新展開)
- Pre-Checkingに基づく効率的スキーママッチングアルゴリズム(LAシンポジウム(情報基礎理論ワークショップ)論文小特集)
- Pre-checkingを用いた効率的2階述語マッチングアルゴリズム (計算理論とアルゴリズムの新展開)
- スキーママッチングを用いたLK類推証明システムの開発
- スキーママッチングとその計算量
- スキーママッチングにおける計算の複雑さ (計算モデルとアルゴリズム)
- スキーママッチングの計算の複雑さ
- 時間的差分データの監視を目的とした携帯端末画面への表示システムに関する研究
- 特集「定理証明, 推論関係の新技術」にあたって
- 様相論理に基づく論理型知識表現言語(計算アルゴリズムの基礎理論)
- 上昇型定理証明器Hyper Tablauxへの関連性試験の導入
- 上昇型定理証明器 Hyper Tablaux への関連性試験の導入
- 非領域限定式を扱う双方向定理証明器
- トップダウン型分散定理証明システムにおける協調の形態に関する研究
- 一階理論に対する単一名公理の計算法
- HTMLからXMLへの事例ベース変換における複合テキストブロックの取扱い : アライメント等の適用
- 事例に基づくHTML文書からXML文書への半自動変換 : シリーズ型HTML文書における類似性の利用
- 様相論理に基づく知識の表現と推論
- トップダウン型定理証明における補題の有用性 : その実装と評価
- トップダウン型定理証明における補題の有用性 : その実装と評価
- 一階論理コンパイラを用いる分散定理証明システムの実装と性能評価
- 一階論理コンパイラを用いる分散定理証明システムの実装と性能評価
- 決定可能な高階単一化問題に関する研究 (アルゴリズムと計算の理論)
- 単純型付きラムダ計算における証明文法
- 非再帰的な述語サーカムスクリプションの一階論理式への等価変換
- 並列サーカムスクリプションのパラメーター消去手法
- 点別サーカムスクリプションに基づく孤立式の一般化
- 高階ユニフィケーションアルゴリズムの複雑さについて (関数型プログラミングと計算の基礎)
- 高階ユニフィケーションにおける可解なクラスと計算の複雑さ(アルゴリズムと計算量の理論)
- 高階論理ユニフィケーションを用いた知識処理(計算アルゴリズムと計算量の基礎理論)
- 定理証明的手法による再帰方程式から回路の自動設計
- 定理証明的手法を用いた回路自動設計のための変換規則--再帰方程式から回路記述への変換
- 回路自動合成のための推論機構(計算アルゴリズムの基礎理論)
- 時間と空間を扱う様相述語論理の不完全性とその相対的完全化
- 定理証明的手法を用いた回路の自動合成 : 帰納方程式から回路への変換(アルゴリズムの数学的基礎理論とその応用)
- プログラム理論と様相論理 (様相論理)
- エージェントの行動学習問題におけるGAとGPの特性解析とハイブリッド化による性能向上
- 構造類似性を考慮した HTML 文書から XML 文書への変換について
- 構造類似性を考慮した HTML 文書から XML 文書への変換について
- HTML文書からXML文書への変換について
- [招待論文]一般単一化理論(「21世紀の知識情報科学に向けて」,及び一般)
- 事例に基づくシリーズ型HTML文書の意味論理構造の自動認識 : HTMLからXMLへの自動変換を目指して
- PTTP型定理自動証明におけるゴールの準最適な並び
- PTTP型定理証明におけるゴールの準最適な並び
- 一般単一化理論
- 2 リテラル節補題の利用による定理証明の高速化
- 2 リテラル節補題の利用による定理証明の高速化
- 補題の一般化による定理証明の高速化
- マルチエージェントシステム分散協調問題における時間遅れと知識量の関係
- 利己的なマルチエージェント群の分散協調における時間遅れの影響
- 遺伝的プログラミングを用いた命題MEタブロー法による定理自動証明
- GPを用いたMEタブロー法による定理自動証明 : 予備的考察
- 近年の定理自動証明技術 : システムコンペCASCとその周辺(「定理証明, 推論関係の新技術」)
- 型付ラムダ計算における証明文法
- 類似性に基づく一般化知識の獲得と推論