私は修士号の最終試験の準備をしています。これは過去の試験の問題で、本当に混乱しています。どこから始めればよいかわかりません。
私の考えでは、許容できるヒューリスティックは解決ルールであり、解決ルールが許容できることを証明します。そうですか? もしそうなら、解決規則が許容できることを証明するには、どこから始めればよいですか? みんなを助けてくれてありがとう。
定理証明アプリケーションを考えてみましょう。A* アルゴリズムを使用して、最も単純な (最短の) 証明を検索できます。既知の公理と定理が命題論理のホーン節の知識ベースとして表され、証明者が後方連鎖を使用すると仮定します。
(a) 許容できるヒューリスティックを提案する。
(b) 提案されたヒューリスティックが許容できることを証明する
はい、定理証明とは、それが一種の解決策であることを意味します。
ホーン節は、明確な節または整合性制約のいずれかです。つまり、Horn 節の先頭には false または通常のアトムがあります。
整合性制約は、
false←a1∧...∧ak という形式の句です。
完全性制約により、システムは、知識ベースのすべてのモデルでアトムの結合が偽であることを証明できます。つまり、アトムの否定の論理和を証明
できます。ホーン節の知識ベースは、アトムの否定を暗示することができます
。例: 知識ベース KB1 を考えてみましょう:
false←a∧b.
a←c.
b←c.
アトム c は、KB1 のすべてのモデルで false です。KB1 のモデル I で c が真である場合、I で a と b の両方が真になります (そうでなければ、私は KB1 のモデルではありません)。I では false が false であり、I では a と b が true であるため、I では最初の節が false であり、I が KB1 のモデルであることに矛盾します。したがって、KB1 のすべてのモデルで c は false です。これは、KB1 ¬c として表されます。これは、¬c が KB1 のすべてのモデルで真であり、したがって、KB1 のすべてのモデルで c が偽であることを意味します。