1994 Fiscal Year Annual Research Report
| Project/Area Number |
06780307
|
|---|
| Research Institution | Toyohashi University of Technology |
|---|
Principal Investigator |
井上 克巳 豊橋技術科学大学, 工学部, 助教授 (10252321)
|
|---|
| Keywords | 定理証明 / 高次推論 / 様相論理 / 様相タブロ-法 / モデル生成 / マジック・セット法 / 非単調推論 / 論理プログラミング |
|---|
| Research Abstract |
高度問題解決における推論手続きを一階述語論理定理証明器上で実現する方法を開発し、いくつかの高次推論系に適用できることを確認した。本年度の研究実績は以下の通りである。
1.本研究においてベースとした一階述語論理定理証明器は、モデル生成方式に基づく高速なボトムアップ型証明器であるMGTPである。このMGTPの性能をさらに向上させるため、トップダウン的なゴール情報を取り入れた探索制御方式(ノンホーン・マジックセット、NHM)の検討を行った。NHMが充足不能性判定問題に対して健全かつ完全であること、およびPrologのSLD導出を用いるSATCHMOREと等価であることを証明した。本NHMは以下に述べる推論処理系の効率化にとって非常に重要である。
2.各種高次推論体系(とくに各種様相理論系と各種非単調推論系)から一階述語論理への等価変換方式を検討し、各種論理から一階述語論理へのコンパイラを開発した。またいくつかの実験を通じてシステムの評価を行い、さらなる改良点について検討した。
3.様相論理系では、証明すべき様相論理式をMGTPの入力節に変換する様相節変換法とその拡張方式を開発した。様相節変換法は、様相体系に応じた可能世界間の到達可能関係の性質をMGTP節として記述することにより、様々な様相体系の定理証明器に拡張可能である。またボトムアップに到達可能関係を計算した場合の無限ループを回避するために、上記NHMを応用し、到達可能関係の計算をトップダウン制御する方式を考案した。
4.非単調推論系では、拡張論理プログラムに基づく知識システム(デフォルト推論、閉世界仮説、矛盾除去、アブダクションへ応用可能)、矛盾を局所的に取り扱う多値論理に基づく拡張選言的データベース、選言付論理プログラミングにおける否定情報の推論(特に極小モデル意味論と可能世界意味論)、等の計算手続きとして、MGTPへのコンパイルが可能であることを示した。
|
-
[Publications] Katsumi Inoue: "Hypothetical Reasoning in Logic Programs" Journal of Logic Programming. 18. 191-227 (1994)
-
[Publications] Chiaki Sakama and Katsumi Inoue: "Paraconsistent Stable Semantics for Disjunctive Programs" Journal of Logic and Computation. (現在印刷中). (1995)
-
[Publications] Chiaki Sakama and Katsumi Inoue: "An Alternative Approach to the Semantics of Disjunctive Logic Programs and Deductive Databases" Journal of Antomated Reasoning. 13. 145-172 (1994)
-
[Publications] 赤植淳一,井上克巳,長谷川隆三: "様相節交換に基づくボトムアップ型様相論理証明法" 情報処理学会誌論文誌. 36(掲載決定). (1995)
