トップダウン型定理証明における補題の有用性 : その実装と評価
スポンサーリンク
概要
- 論文の詳細を見る
Stickel により開発されたPTTPは,一階論理コンパイラであり,証明すべき一階論理式が与えられると,その上のModel Elimination を模倣する Prolog プログラムを出力する.出力コードはそれ自身極めて高速に動作するが,トップダウン型の証明を行なう(模倣する)ために,同一解の再計算を頻繁に行なうという本質的な問題を持っている.本研究では,トップダウン型証明法における再計算の抑制を目的として,中間の計算結果を補題化し,生成された補題を参照することによって証明を高速化する手法を検討する.幾つかの手法を考察し,PTTPに実装,性能評価実験を行なった.
- 一般社団法人情報処理学会の論文
- 1994-09-20
著者
関連論文
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(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とその周辺(「定理証明, 推論関係の新技術」)