一阶述语论理.ppt

*  第8回　 一階述語論理 　 　 *  　述語論理(predicate calculus, logic) 種々の知識を表現するための形式的言語～　第１階述語論理 知識を記号の式として数学的に表現 cf）述語：　真偽判定可能な叙述 例）　(?Ｘ)(elephant(X) → color(X, gray)) 理論的基盤が保証されている 導出原理(resolution principle)による推論 人間の持つ曖昧性を組み込むことが困難 　 知識表現の種類と特徴-７　 *  個体への言及不可　　　～記述の最小単位：命題 例）?p:「全ての日本人は人間」　?q:「太郎は日本人」→　r:「太郎は人間」　　が導出できない 　　～ (p∧q)→rは恒真命題でない 　 命題論理の限界 *  個体に注目し，「個体について何が述べられているか」という観点から命題の内部構造を記述 対象領域：　議論の対象となる個体の集合??x[J(x)→M(x)]?J(a) 　 a:太郎 →　M(a) 一階述語論理：　個体についてのみ変数を認める述語論理～　完全な演繹体系　α|=β →　 α|-β 　 述語論理への拡張 *  健全(sound): 証明論的方法で恒真性を示した命題が，常に，意味論的にも恒真性を保証されている場合α|-β →　 α|=β 完全（complete): 意味論的に恒真の論理式が与えられた場合，それが恒真であることを導く論理式操作（証明論的手法）が常に存在する場合 α|=β →　 α|-β 複雑な論理体系～　健全だが不完全 　 基本的な概念　-3 *  定数 （個体）変数：　 X, Y 関数記号：　plus(X, Y) 述語記号：　red(X)、study(x, school, English) 論理結合子：　-連言(conjunction): ∧　選言(disjunction): ∨ -否定(negation): ￢　　　含意(implication): → 束縛（量）記号： -全称記号: ? 存在記号: ? 補助記号：　（），，?? 　 述語論理表現に用いる記号（統語論） *  一階述語論理の論理式が充足不能（恒偽）かどうかを判定する部分的決定手続き 冠頭標準形への変換 Skolem標準形への変換 節集合への変換?融合の実行 代入 単一化 融合節の生成 空節の導出 　 融合法 *  素（原子）命題：　述語記号と項から構成される命題 リテラル(literal)：　素命題、または素命題の否定 節(clause)：　リテラル、またはリテラルの選言 節形式命題：　 Skolem標準形 (?x1) (?x2) ?? (?xn)[C1∧C2 ∧ ??∧Cm][]内：　母式(matrix) 　 節形式 *  対象領域D, 論理式M[x]に対し， ?ｘ [M[x]]が真であることを示すのは困難 一方， ?a∈Dに対し， M[a]が偽であることを示せば　恒偽式であることは示せる 　 融合法（背理法）の原理 *  冠頭標準形：論理式F:　(Q1x1)???(Qnxn)α(Q1x1)???(Qnxn)：冠頭部　α：本体　Qi:束縛子 P → Qを￢P∨Qに、Ａ≡Ｂを（ ￢Ａ∨Ｂ）∧（ ￢Ｂ∨Ａ）に変換 否定記号の括り出し： ￢（￢Ａ）=Ａ ￢（Ａ∧Ｂ）= （ ￢Ａ∨￢Ｂ） ￢（Ａ∨Ｂ）= （ ￢Ａ∧￢Ｂ） ￢ ((?x)α）= (?x)(￢α)  ￢ ((?x)α）= (?x)(￢α) 　 節形式への変換-1 *  Skolem標準形への変換 連言標準形へ変換 存在記号?の除去： (?x) (?y)P(x,y) = (?x) P(x, f(x)) 　　　 f(x):　Skolem関数存在記号を含む変数を引数とする新しい関数で置き換えたもの 　 節形式への変換 -2 *  ?x?y[P(x,y)→Q(x)]∧￢ (?y [P(y)→￢R(y)] ∧?z R(z)) =?x?y[￢P(x,y)∨Q(x)]∧ ￢(?y [￢P(y)∨￢R(y)] ∧?z R(z)) = ?x?y[￢P(x,y)∨Q(x)]∧(?y [￢(￢P(y)∨￢R(y)) ∨ ￢(?z R(z)) ] =?x?y[￢P(x,y)∨Q(x)]∧(?y [(P(y)∧R(y)] ∨?z[￢R(z)]] =?x1?y1[￢P(x1,y1)∨Q(x1)]∧(?y2 [(P(y2)∧R(y2)]∨?z1[￢R(z1)]] ＝　?x1[￢P(x1,f(x1))∨Q(x1)]∧(?y2 [(P(y2)∧R(y2)] ∨￢R(g(y2)) =?x1?y2 [(￢P(x1,f(x1