2 リテラル節補題の利用による定理証明の高速化
スポンサーリンク
概要
- 論文の詳細を見る
トップダウン型の定理証明法が本質的に備えている同一解の再計算という問題を解決するため、中間の計算結果を補題化し、生成された補題を参照することでこれらの冗長な再計算を回避する手法が提案され、実際に利用されている。補題をトップダウン型の定理証明器に組み込む場合、実装の容易さから単位節補題がしばしば利用されるが、単位節補題で簡約できる冗長な再計算には限界があり、さらなる探索空間の縮小のためには非単位節補題の導入が必要となる。本研究では限定された形の非単位節補題として、2 リテラル節補題を実装するとともに、複数の 2 リテラル節補題の利用法を提案し、実験によってもっとも効果的な利用法を考察する。
- 社団法人電子情報通信学会の論文
- 1999-03-05
著者
関連論文
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(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とその周辺(「定理証明, 推論関係の新技術」)