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

• Item type: SIG Technical Reports(1)
• 公開日: 1995-06-16
• タイトル: 停止性を保証する汎用様相論理定理証明手続き
• タイトル / 言語: en
• タイトル: A Uniform Theorem Proving Method for Modal Logics with Termination
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: NTTコミュニケーション科学研究所
• 著者所属(英): en
• 著者所属(英): NTT Communication Science Laboratories
• 著者名: 櫟粛之
• 著者名(英): Tadashi, Araragi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究では、いくつかの様相論理体系に対して、統一的な立場で、停止性を保証する証明手続きを与える。我々は、[Ara 1]、[Ara 2]において、一階述語論理式で特徴づけられるKripke frameのクラスに対し完全となる正則体系の全体に対して、統一的に適用できる証明手続きを与えた。この手続きは、prefixed tableau法（[Fit]）の考えを一般化したもので、一階述語論理式Σによって特徴づけられる体系S_Σに対して、「S_Σ 〓 φ ⇔あるμ ∈Nがあり、Σ〓_<POL> Δ（φ）_μ」となる一階述語論理式Δ（φ）_μを構成する手続きである。この方法による証明手続きは、体系がdecidableであっても、停止性を保証するとは限らない。それは、Σ〓_<POL> Δ（φ）_μかどうかをチェックする一階述語論理の定理証明手続きが停止性を保証しないこと、φがS_Σの定理でない場合、全てのμに対してΣ〓_<POL> Δ（φ）_μをチェックしなければならないことによる。本研究では、ある種の体系に対して、φの形から、Σ〓_<POL> Δ（φ）_μの証明探索が有限の範囲に限定でき、またチェックすべきΣ〓_<POL> Δ（φ）_μのμの最大値を評価する手法を与えた。これにより、S_Σ 〓 φか否かのチェックが有限回のステップで終了する証明手続きが得られる。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a new method of giving a theorem proving procedure with termination for some modal logics, from a uniform point of view. In [Ara1] and [Ara2], we gave a uniform theorem proving method for normal systems which are complete for a class of Kripke frames characterized by a first-order formula. This procedure, based on the idea of the prefixed tableau method [fit], constructs first order formulas Δ(φ)_μ for each natural number μ with the property: S_Σ 〓 φ iff for some μ ∈N, Σ〓_<POL> Δ(φ)_μ, where S_Σ is the system characterized by the first-order formula Σ. This proving procedure does not guarantee the termination even for decidable systems. It is because theorem proving of Σ〓_<POL> Δ(φ)_μ in the first-order logic does not terminate in general and, if φ is not a theorem of S_Σ ,we have to check Σ〓_<POL> Δ(φ)_μ for all μ. In this paper, for some modal logics, we give a uniform method of obtaining the information from a formula φ which enables us to reduce the proof search of Σ〓_<POL> Δ(φ)_μ to finite steps and gives an upper bound of μ which ensures that there is no proof for Σ〓_<POL> Δ(φ)_μ for any μ if there is not for any μ below the bound. Hence, we get the theorem proving method with termination for the modal logics.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1995, 号 58(1995-PRO-001), p. 17-24, 発行日 1995-06-16
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会