停止性を保証する汎用様相論理定理証明手続き

概要

論文の詳細を見る
本研究では、いくつかの様相論理体系に対して、統一的な立場で、停止性を保証する証明手続きを与える。我々は,[Ara 1]、[Ara 2]において、一階述語論理式で特徴づけられるKripke frameのクラスに対し完全となる正則体系の全体に対して、統一的に適用できる証明手続きを与えた。この手続きは、prefixed tableau法([Fit])の考えを一般化したもので、一階述語論理式Σによって特徴づけられる体系S_Σに対して、「S_Σ|-φ⇔あるμ∈Nがあり、Σ|-_<FOL>△(φ)_μ」となる一階述語論理式△(φ)_μを構成する手続きである。この方法による証明手続き,は、体系がdecidableであっても、停止性を保証するとは限らない。それは、Σ|-_<FOL>△(φ)_μかどうかをチェックする一階述語論理の定理証明手続きが停止性を保証しないこと、φがS_Σの定理でない場合、全てのμに対してΣ|-_<FOL>△(φ)_μをチェックしなければならないことによる。本研究では、ある種の体系に対して、φの形から,Σ|-_<FOL>△(φ)_μの証明探索が有限の範囲に限定でき,またチェックすべきΣ|-_<FOL>△(φ)_μのμの最大値を評価する手法を与えた。これにより,S_Σ|-φか否かのチェックが有限回のステップで終了する証明手続きが得られる。
1995-06-16