Prologにおける再帰式の正当性に関するある十分条件

• Item type: SIG Technical Reports(1)
• 公開日: 1987-09-17
• タイトル: Prologにおける再帰式の正当性に関するある十分条件
• タイトル / 言語: en
• タイトル: Sufficient Conditions for Validity of Recursion Formula in Prolog
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: （株）日立製作所基礎研究所
• 著者所属: （株）日立製作所基礎研究所
• 著者所属(英): en
• 著者所属(英): Advanced Research Laboratory, Hitachi Ltd.
• 著者所属(英): en
• 著者所属(英): Advanced Research Laboratory, Hitachi Ltd.
• 著者名: 櫻井, 彰人; 元田, 浩
• 著者名(英): Akito, Sakurai; Hiroshi, Motoda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 確定節によって表現される形式、とくに再帰形式（確定節の頭部の述語がその本体部にも現われる）が確定節のある集合から導かれる（その集合に対し正当である）ための十分条件を示す。一般に確定節の正当性を証明するには数学的帰納法を用いる必要があるが、数学的帰納法を自動的に適用するには帰納仮説の発見、証明過程での仮説の使用など、通常発見的に行なわれる推論を自動化しなければならない問題がある。本報告で提示する十分条件は、それが実際に満足されているか否かどうかは数学的帰納法を用いずに確かめることができる。そして、結果的に数学的帰納法が必要になる証明を、数学的帰納法を用いずに証明することを可能とするものである。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: A new approach for proving validity of recursive formuli written in definite clauses is developed based on resolution and definite clauses as functions. The main problem, when automatically proving it, is to develop strategy for inductive proof, or how to find out an appropriate induction scheme and how to direct deductions. We propose a method to prove some properties on definite clauses without induction, which eventually satisfy sufficient conditions for formuli to hold. We first prove sufficient conditions stated in terminology of functions, and then convert them to the ones stated in resolution equivalent to unfold transformation. We also prove a Prolog version of the fixed point induction and extend it.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11135936
• 書誌情報: 情報処理学会研究報告知能と複雑系（ICS）; 巻 1987, 号 63(1987-ICS-054), p. 1-8, 発行日 1987-09-17
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会