一階理論に対する単一名公理の計算法
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,Clarkの等号理論を仮定した場合の等号を含む一階式の定理証明技法を考察する.Clarkの等号理論は単一名仮説の拡張になっており,常識推論において,有用な結論を導くためにしばしば用いられる.Clarkの等号理論を一階式と同時に仮定し,導出原理を用いて定理証明を行なおうとした場合,スコーレム関数の影響によってClarkの等号理論は通常のユニフィケーションアルゴリズムでは計算できなくなる.そこで本論文では,このための新たな計算法を導入する.まずClarkの等号理論を,スコーレム関数以外の関数のみに仮定できるように拡張する.次に,これを導出原理に基づく定理証明法に組み込む.さらに,扱う節を許容的(allowed)なものに制限した場合,計算が効率的に行なわれることを示す.
- 日本ソフトウェア科学会の論文
- 1995-03-15
著者
関連論文
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(1997-2001)
- 投機的計算によるSATプランニングの効率改善に関する研究(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- 超高速ATM LANの構築法と次世代ユーザーインタフェースに関する研究
- 時間的差分データの監視を目的とした携帯端末画面への表示システムに関する研究
- 特集「定理証明, 推論関係の新技術」にあたって
- 上昇型定理証明器Hyper Tablauxへの関連性試験の導入
- 上昇型定理証明器 Hyper Tablaux への関連性試験の導入
- 非領域限定式を扱う双方向定理証明器
- トップダウン型分散定理証明システムにおける協調の形態に関する研究
- 一階理論に対する単一名公理の計算法
- HTMLからXMLへの事例ベース変換における複合テキストブロックの取扱い : アライメント等の適用
- 事例に基づくHTML文書からXML文書への半自動変換 : シリーズ型HTML文書における類似性の利用
- トップダウン型定理証明における補題の有用性 : その実装と評価
- トップダウン型定理証明における補題の有用性 : その実装と評価
- 一階論理コンパイラを用いる分散定理証明システムの実装と性能評価
- 一階論理コンパイラを用いる分散定理証明システムの実装と性能評価
- 非再帰的な述語サーカムスクリプションの一階論理式への等価変換
- 並列サーカムスクリプションのパラメーター消去手法
- 高階ユニフィケーションアルゴリズムの複雑さについて (関数型プログラミングと計算の基礎)
- エージェントの行動学習問題におけるGAとGPの特性解析とハイブリッド化による性能向上
- 構造類似性を考慮した HTML 文書から XML 文書への変換について
- 構造類似性を考慮した HTML 文書から XML 文書への変換について
- HTML文書からXML文書への変換について
- 事例に基づくシリーズ型HTML文書の意味論理構造の自動認識 : HTMLからXMLへの自動変換を目指して
- PTTP型定理自動証明におけるゴールの準最適な並び
- PTTP型定理証明におけるゴールの準最適な並び
- 2 リテラル節補題の利用による定理証明の高速化
- 2 リテラル節補題の利用による定理証明の高速化
- 補題の一般化による定理証明の高速化
- マルチエージェントシステム分散協調問題における時間遅れと知識量の関係
- 利己的なマルチエージェント群の分散協調における時間遅れの影響
- 遺伝的プログラミングを用いた命題MEタブロー法による定理自動証明
- GPを用いたMEタブロー法による定理自動証明 : 予備的考察
- 近年の定理自動証明技術 : システムコンペCASCとその周辺(「定理証明, 推論関係の新技術」)