Prologによる定理証明の一方法

• Item type: SIG Technical Reports(1)
• 公開日: 1987-02-13
• タイトル: Prologによる定理証明の一方法
• タイトル / 言語: en
• タイトル: A Theorem - Proving Method in Prolog
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京電機大学理工学部
• 著者所属: 東京電機大学理工学部
• 著者所属(英): en
• 著者所属(英): School of Science and Engineering, Tokyo Denki University
• 著者所属(英): en
• 著者所属(英): School of Science and Engineering, Tokyo Denki University
• 著者名: 松浦, 聡; 中村, 克彦
• 著者名(英): Satoshi, Matsuura; Katsuhiko, Nakamure
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Prologを用いて述語論理の定理証明を行う場合，Prologが一般の節ではなくホーン節を基礎としていることが問題となる。この報告では，副目標として含意を含んだ論理式が書けるように拡張したホーン節を用いて定理証明を行う方法を提案する。この報告では，このように拡張した目標（拡張目標）を含む節を用いることによって，つぎのふたつが成立することが示される。(1)一般の節集合と等価な論理式を拡張した節の集合に変換できる。(2)健全(sound)で完全(complete)な述語論理の証明手続きを構成することができる。この証明手続きはassert機能を用いてProlog上にインプリメントできる。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: A problem for proving theorems of predicate logic using a Prolog system is that Prolog is based on Horn clauses and not on the general clauses. This report presents a theorem-proving method in that the Horn clauses are extended to have the expressions with implication operators as the subgoals. The following two propositions are shown. (1) Any set of the general clauses can be transformed into that of the extended Horn clauses. (2) The proof procedure base on the method is sound and complete. The procedure can be implemented in the Prolog systems by using the assert function.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1987, 号 10(1986-PRO-020), p. 1-8, 発行日 1987-02-13
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会