証明戦略
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/10/21 06:25 UTC 版)
導出は２つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについては様々な選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。 線形導出（linear resolution） 前提となる節の一方を、頂上節（top clause）として指定した節と、頂上節から導出された節に限定する方法。導出木を書くと導出の流れが線状に一列に並ぶため、線形導出と呼ばれる。論理プログラミング言語の代表であるPrologで用いられるSLD導出（Selective Linear resolution for Definite clause）は線形導出の一種である。 入力導出（input resolution） 前提となる節の一方を最初に与えられた節集合の要素（導出された節以外の節）に限定する方法。 支持集合戦略（set-of-support strategy） あらかじめ支持集合という節の集合を指定しておき、前提となる節の一方を支持集合の節とそこから導出された節に限定する方法。節集合S、T がありS-T が充足可能であるときT はS の支持集合と言う。目標に関係ないところを探索しないよう導出の対象を制限することで、より効率的な導出を行うための手法で、1965年に Lawrence Wos らが提案した。 意味導出（semantic resolution） 論理式のモデルあるいは解釈を利用して導出の対象を制限し、探索の空間を狭めることで効率的な導出を行う手法。特定のモデルにおいて真となる可能性がある節と偽となる可能性のある節とを親節に選ぶ Slagle の Semantic Clash resolution など様々な方法がある。
※この「証明戦略」の解説は、「導出原理」の解説の一部です。
「証明戦略」を含む「導出原理」の記事については、「導出原理」の概要を参照ください。
- 証明戦略のページへのリンク
