9

命題論理における解決規則が何であるかを理解することができませんでした。決議は、文を拡張して別の形式で書くことができるいくつかの規則を単に述べていますか？
以下は、命題論理の単純な解決アルゴリズムです。この関数は、2つの入力を解決することによって取得されたすべての可能な句のセットを返します。アルゴリズムの動作が理解できません。誰かが説明してもらえますか？

  function PL-RESOLUTION(KB,α) returns true or false
     inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a
             sentence in propositional logic 
     clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α
     new <--- {}
     loop do
        for each Ci, Cj in clauses do
            resolvents <----- PL-RESOLVE(Ci, Cj)
            if resolvents contains the empty clause then return true
            new <--- new ∪ resolvents
        if new ⊆ clauses then return false
        clauses <---- clauses  ∪ new
4

3 に答える 3

15

これは議論のトピック全体ですが、簡単な例を 1 つ説明しようと思います。

アルゴリズムの入力はKB - 解決を実行するためのルールのセットです。次のような一連の事実として理解するのは簡単です。

  1. りんごは赤い
  2. smthが赤ならこのsmthは甘い

R(x)- ( x is red ) とS(x)- ( x is sweet )の 2 つの述語を紹介します。正式な言語で事実を書くことができるよりも：

  1. R('apple')
  2. R(X) -> S(X)

¬R v S解決規則の対象となるとして、2 番目の事実を代用できます。

プログラムで解決ステップを計算すると、2 つの相反する事実が削除されます。

例: 1) a & ¬a -> empty. 2)a('b') & ¬a(x) v s(x) -> S('b')

2 番目の例では、変数xが実際の値に置き換えられていることに注意'b'してください。

文apple が甘いかどうかを判断するプログラムの目標は true です。この文も形式言語で と書きS('apple')、逆さまにして質問します。問題の正式な定義は次のとおりです。

  • 条項1 =R('apple')
  • 条項2 =¬R(X) v S(X)
  • ゴール？=¬S('apple')

アルゴリズムは次のように機能します。

  1. 節 c1 と c2 を取る
  2. c1 と c2 のリゾルベントを計算すると、新しい句 c3 = が得られます S('apple')
  3. c3 のリゾルベントを計算すると、goal によって空のセットが得られます。

つまり、私たちの文は真実です。そのような解像度で空のセットを取得できない場合は、文が誤りであることを意味します (ただし、実際のアプリケーションのほとんどの場合、KB の事実が不足しています)。

于 2012-09-17T15:53:19.723 に答える
4

X = {a, x1, x2, ..., xm} および Y = {~a, y1, y2, ..., yn} の節 X および Y を考えます。ここで、a は変数であり、~a はその変数です。否定であり、xi と yi はリテラル (つまり、否定される可能性のある変数) です。

X の解釈は命題 (a \/ x1 \/ x2 \/ ... \/ xm) です。つまり、X が真であると仮定すると、a の少なくとも 1 つまたは xi の 1 つが真でなければなりません。Yさんも同様。

X と Y が真であると仮定します。

また、a の値に関係なく、(a \/ ~a) が常に真であることもわかっています。

~a が真の場合、a は偽であるため、~a /\ X => {x1, x2, ..., xm}.

a が true の場合、~a は false です。この場合、a /\ Y => {y1, y2, ..., yn}.

したがって、X と Y が真であると仮定すると、{x1, x2, ..., xm, y1, y2, ..., yn} は真でなければならないことがわかります。new 節が変数 a を参照していないことに注意してください。

この種の控除は、解像度として知られています。

これは、解像度ベースの定理証明器でどのように機能しますか? シンプル: 矛盾による証明を使用します。つまり、「事実」を節に変えることから始め、「目的」の否定に対応する節を追加します。その後、最終的に空節 {} に解決できれば、空節は虚偽に等しいため、矛盾に達したことになります。事実が与えられているので、これは否定されたゴールが間違っているに違いないことを意味し、したがって (否定されていない) ゴールは真でなければなりません。

于 2012-09-18T04:33:28.040 に答える
0

解決は、述語論理で表現可能な引数が正しいことを証明するために使用される手順であり、命題論理における文の反駁定理証明手法
に つながります。 決議は、反駁による証拠を提供します。すなわち、それが有効であることを示すために、解決は、ステートメントの否定が既知のステートメント アルゴリズムと矛盾することを示すことを試みます: 1)。公理のすべての命題を節形式 2) に変換します。命題を否定し、結果を節形式に変換する 3)それらを解決する 4)解決者が空の節である場合、矛盾が見つかった





于 2012-09-21T20:30:09.457 に答える