非領域限定式を扱う双方向定理証明器
スポンサーリンク
概要
- 論文の詳細を見る
本論文では、非領域限定式を対象とする双方向定理証明器に関する理論的な枠組について考察を行なう。任意の一階節集合を扱うために、SATCHMOREやMGTPで利用されているモデル生成法の拡張を試みる。この拡張のために、単一化機構によるモデル候補を保持を可能とする。
- 社団法人電子情報通信学会の論文
- 1996-11-02
著者
関連論文
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(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とその周辺(「定理証明, 推論関係の新技術」)