高度問題解決のための定理証明技法の研究

点击翻译按钮获取中文摘要

高度問題解決における推論手続きを一階述語論理定理証明器上で実現する方法を開発し、いくつかの高次推論系に適用できることを確認した。本年度の研究実績は以下の通りである。1.本研究においてベースとした一階述語論理定理証明器は、モデル生成方式に基づく高速なボトムアップ型証明器であるMGTPである。このMGTPの性能をさらに向上させるため、トップダウン的なゴール情報を取り入れた探索制御方式(ノンホーン・マジックセット、NHM)の検討を行った。NHMが充足不能性判定問題に対して健全かつ完全であること、およびPrologのSLD導出を用いるSATCHMOREと等価であることを証明した。本NHMは以下に述べる推論処理系の効率化にとって非常に重要である。2.各種高次推論体系(とくに各種様相理論系と各種非単調推論系)から一階述語論理への等価変換方式を検討し、各種論理から一階述語論理へのコンパイラを開発した。またいくつかの実験を通じてシステムの評価を行い、さらなる改良点について検討した。3.様相論理系では、証明すべき様相論理式をMGTPの入力節に変換する様相節変換法とその拡張方式を開発した。様相節変換法は、様相体系に応じた可能世界間の到達可能関係の性質をMGTP節として記述することにより、様々な様相体系の定理証明器に拡張可能である。またボトムアップに到達可能関係を計算した場合の無限ループを回避するために、上記NHMを応用し、到達可能関係の計算をトップダウン制御する方式を考案した。4.非単調推論系では、拡張論理プログラムに基づく知識システム(デフォルト推論、閉世界仮説、矛盾除去、アブダクションへ応用可能)、矛盾を局所的に取り扱う多値論理に基づく拡張選言的データベース、選言付論理プログラミングにおける否定情報の推論(特に極小モデル意味論と可能世界意味論)、等の計算手続きとして、MGTPへのコンパイルが可能であることを示した。