効率的時間論理証明システムの構成

• Item type: SIG Technical Reports(1)
• 公開日: 1987-12-10
• タイトル: 効率的時間論理証明システムの構成
• タイトル / 言語: en
• タイトル: Construction of Efficient Theorem Proving System for Temporal Logic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京工業大学工学部情報工学科
• 著者所属: 東京工業大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Tokyo Institute of Technology
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Tokyo Institute of Technology
• 著者名: 米崎, 直樹; 端山, 毅
• 著者名(英): Yonezaki, Naoki; Hayama, Takeshi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本時間論理証明システムは、様相記号の統一化の概念を用いた一般的様相論理証明器を時間論理に適用したものである。基本的な証明手続きは、結合法に基づいている。様相論理の体系による違いは様相記号列の統一化規則にのみ反映される。この一般的様相論理証明器を線形時間に適用し、next-time(○)を加えて、時間論理に拡張した。本時間論理証明システムの特徴は、証明手続き全体が幾つかの部分手続きに分解されるため、部分手続き毎に効率化が可能であり、有効な戦略の追加による効率化が期待できることである。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: A new theorem proving system for propositional temporal logic is presented. This systemis based on the conection method in which unification of modal operator sequences is used. Only constraint of the unification refrects diference of various modal logic systems. Firstly, the unification constraint and general proof procedure are exprained. Then, we specialize the method for lineir time tempral logic by introdusing next time operators. The problem of deciding the satisfiability of the formulas for the logic is PSPACE-complete, however, it is possible to introduce stratrgies for the algorithm in order to get efficiency for general cases. By formalizing the system in our frame work, it becomes possible to find out some heuristics in each prooving step.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1987, 号 89(1987-PRO-023), p. 79-88, 発行日 1987-12-10
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会