[[Logic & ILP 用語・定理集]]

 

内容一覧

解釈 (Interpretation)

  • 定義2.15 A pre-interpretation J of a first-order language L consists of the following:
    1. A non-empty set D, called the domain of the pre-interpretation.
    2. Each constant in L is assigned an element of D.
    3. Each n-ary function symbol f in L is assigned a mapping Jf from Dn to D.
  • (コメント)
    • 関数記号、例えばf、とは関数の名前である。
    • 関数の実体はラムダ関数形式で記述するといいのかも知れない。
      関数の実体λx = x + 1, 関数の名前f.
      つまり、 (define function f (lambda (x) (plus x 1)))
      ということ。
    • 解釈と前解釈との違いに注意。このあたりの内容を正しく理解する1つのポイントです。
    • なぜ前解釈というものを設定するのかは先まで勉強すればわかります。

    1. 記号fを名前とする関数λx(x + 1))を考える。この場合f(a), f(f(a))を考えることができる。では、f(a)はどういう解釈ができるであろうか? これを考える。
      さて、いまさらに自然数というものを考える。そこでいま定数記号aに数字ゼロを対応させることにする。つまり、aはゼロを表す記号とする。すると、
      f(a)=λx(x+1)(a)=a+1=0+1=1
      f(f(a))=2;
      となることより、f(a)とf(f(a))はそれぞれイチとニを表していること、そのように解釈することができることを意味している。
      前解釈とは、与えられた論理式における定数や関数に実体としての意味を与える作業のことであり、この準備の後論理式自体の真偽を考えることになる。その意味で、解釈の準備としての解釈(前解釈)である。
    2. Pre-XXXという表現としては、他には例えば、pre-Banach空間やpre-Hilbert空間などがある。"pre"という接頭語はまだ必要なものが揃っていない( 完備されていない)という気持ちを表している。

変数割当て (Variable assignment)

  • 定義2.17 (Variable assignment) Let J be a pre-interpretation with domain D of a first-order language L.  A variable assignment V with respect to L is a mapping from the set of variables in L to the domain D of J.
    We use V(x/d) to denote the variable assignment which maps the variable x to d ∊ D, and maps the other variables according to V.

Herbrand Models

  • 命題3.30(Herbrabdモデルの意義) Let Σ be a set of clauses in a first-order language L. Then Σ has a model iff(if and only if) Σ has a Herbrand model.
    Σを一階述語言語で書かれた節集合とする。このとき、Σがモデルを持つのは、Σがエルブランモデルを持つとき、そしてそのときに限る。
    • (コメント)一階述語言語で書かれた節集合では、 モデルを持つこととエルブランモデルを持つこととは同じことである、ということ。 一般に、一階述語論理式に適合するモデル(解釈)が存在するかどうかを知るためには、 あらゆる場合(ここが要点!)について調べてみなければならない。 例えば、P(a)という単純な論理式を取り上げ、その論理式にモデルが存在するか否かを考えてみよう。 まず、モデルが存在するか否かを調べるために、あらゆる解釈を考えることになる。 その後その解釈がモデルとなり得るのかを調べる。 この際、この述語名Pにはどのような解釈を与えてもよく、定数aはどのようなものを指していてもよい。 まさに無限個の可能性をコツコツと地道に調べる必要がある。 モデルが存在するのであるならば、その内に見つかるであろう。 しかしながら、モデルが存在しない場合は永遠に様々な解釈を考え、 それがモデルであることを調べ続けることになる。 モデルがないことを示そうとする場合には、このような困難が潜んでいる。 しかしながら上記の命題によれば、エルブランモデルという特殊なモデルだけについて考察し、 もしエルブランモデルが存在すれば、その節集合には(エルブランモデルを含め)何らかのモデルが存在し、 もしエルブランモデルが存在しなければ、エルブランモデルだけではなく他のいかなるモデルも存在しない、 ということを保証してくれている。 この点において上記命題は、極めて意味のある重要な主張である。
    • [証明]
      (I)⇒の証明:
      • Σのpre-interpretationとして、ΣのHerbran pre-interpretationを採用する。
      • いまPをΣ内に現れるアリティnの述語記号とする。このとき、関数Ipを以下のように定義する。
        Ip:UnL→{T,F} ≡ Ip(t1,t2,...,tn)=T if P(t1,t2,...,tn) is true under M,and Ip(t1,t2,...,tn)=F otherwiese.
      • このとき、IはΣのHerbrandモデルである。

        (2)<=の証明:
      • ΣがHerbrandモデルを持つとする。このとき、ΣはHerbrandモデルという名前のモデルを持っている。
  • 命題3.31(Herbrand modelの意義その2) Let Σ be a set of formulae and φ a formula. Let S be a standard form of Σ∪{〜φ}. Then Σ|= φ iff S has no Herbrand models.

包摂する(Subsume)

  • 定義5.2 Let C and D be clauses. We say that [C subsumes D] if there exists a '[substitution]' θ such that Cθ⊆D (i.e., every literal in Cθ also apears in D). Subsumption is also sometimes called θ-subsumption.
    CとDを節とする。[CがDを包摂する]とは、Cθ⊆Dが成り立つ(すなわち、CθのどのリテラルもDの要素になっている)ような[代入]θが存在することである。包摂はしばしばθ包摂とも呼ばれる。
    1. C=P(x) subsumes D=P(a)∨Q(x).
    2. C=P(a)∨P(a) subsumes D=P(a). D also subsumes C.
    3. C=P(x)∨〜Q(a) subsumes D=P(a)∨〜P(f(x))∨〜Q(a).
    4. 空節□ subsumes any clause.
    5. 空節□ subsumes 空節□ itself.
  • 包摂の意味について:  包摂とは、本来「ある範囲中に包み込んでいる、あるいは包み込まれている」という 意味であり、論理学の分野では、AがBを包摂するとは、 AがBを意味的に包み込んでいる、すなわち、AはBの上位概念であることを意味する。 従って例えば以下のような表現が可能である。
    • 概念“動物”は概念“シロクマ”を包摂する。
    • 概念“自然数”は概念“実数”に包摂される。
  • 上記の例aでは、「節P(x) が 節P(a)∨Q(x) を包摂する」となっているがこの意味は 以下の通りである。
    1. 変数xに定数aを代入するとそれぞれP(a), P(a)∨Q(a) となる。
    2. 従って、節{ P(a) } ⊆ 節{ P(a), Q(a) } が成り立つ。
    3. これは上記の定義により 「節C:P(x)が節D:P(a)∨Q(a)を包摂する」ことになる。
    4. つまり、「節Cが真であれば節Dも真である」ということを表現したものである。

演繹する(Deduction; |-d)

  • 定義5.4(Deduction; |-d) Let Σ be a set of clauses and C a cluase. We say that there exists a deduction C from Σ, written as Σ |-d C, if C is a tautology, or if there exists a clause D such that Σ |-r D and D subsumes C. If Σ |-d C, we say that C can be deduced from Σ.

演繹の健全性(Soundness of deduction)

  • 定理5.6(Soundness od deduction) Let Σ be a set of clauses, and C be a clause. If Σ |-d C, then Σ |= C.
    Σを節集合、Cを節とする。このとき、ΣからCが演繹的に導かれるならば、ΣはCのモデルである。

包摂定理(Subsumption Theorem): Σ|=C iff Σ|-d C.&

  • 定理5.17 Subsumption Theorem Let Σ be a set of clauses, and C be a clause. Then Σ|=C iff Σ|-d C.
    Σを節集合、Cを節とする。このとき、CがΣから
  • (コメント)意味論的に証明できるものは統語論的にも証明でき、統語論的に証明できるものは意味論的にも証明できるということ。

理論(Theory)

  • 定義9.1 A [theory] is a finite set of [clauses]. 
    [理論]とは[節]が有限個集まったものである。 [#t33dec21]

節集合Σの否定集合~Σ

  • 定義9.2 If Σ={C1, C2, ... } is a set of clauses, then we use ~Σ to denote {~C1, ~C2, ... }.
    Σ={C1, C2, ... }を節の集まりとするとき、~Σ は{~C1, ~C2, ... }である。 [#a696e3dc]
  • (以下、準備中)

トップ   編集 凍結解除 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2014-08-09 (土) 17:52:21 (1223d)