第8回
一階述語論理
1
知識表現の種類と特徴-７
述語論理(predicate calculus, logic)
種々の知識を表現するための形式的言語
～ 第１階述語論理
知識を記号の式として数学的に表現
cf）述語： 真偽判定可能な叙述
例） (∀Ｘ)(elephant(X) → color(X, gray))
理論的基盤が保証されている
導出原理(resolution principle)による推論
人間の持つ曖昧性を組み込むことが困難
2
命題論理の限界
個体への言及不可
～記述の最小単位：命題
例）・p:「全ての日本人は人間」
・q:「太郎は日本人」
→ r:「太郎は人間」
が導出できない
～ (p∧q)→rは恒真命題でない
3
述語論理への拡張
個体に注目し，「個体について何が述べられてい
るか」という観点から命題の内部構造を記述
対象領域： 議論の対象となる個体の集合
・∀x[J(x)→M(x)]
・J(a)
a:太郎
→ M(a)
一階述語論理：
個体についてのみ変数を認める述語論理
～ 完全な演繹体系 α|=β → α|-β
4
基本的な概念 -3
健全(sound):
証明論的方法で恒真性を示した命題が，常に，
意味論的にも恒真性を保証されている場合
α|-β → α|=β
完全（complete):
意味論的に恒真の論理式が与えられた場合，
それが恒真であることを導く論理式操作（証明論
的手法）が常に存在する場合
α|=β → α|-β
複雑な論理体系～ 健全だが不完全
5
述語論理表現に用いる記号（統語論）
定数
（個体）変数： X, Y
関数記号： plus(X, Y)
述語記号： red(X)、study(x, school, English)
論理結合子：
-連言(conjunction): ∧ 選言(disjunction): ∨
-否定(negation): ￢
含意(implication): →
束縛（量）記号：
-全称記号: ∀
存在記号: ∃
補助記号： （），，・・
6
融合法
一階述語論理の論理式が充足不能（恒偽）かどう
かを判定する部分的決定手続き
1.
冠頭標準形への変換
2.
Skolem標準形への変換
3.
節集合への変換・融合の実行
代入
単一化
融合節の生成
空節の導出
7
節形式
素（原子）命題： 述語記号と項から構成される命題
リテラル(literal)： 素命題、または素命題の否定
節(clause)： リテラル、またはリテラルの選言
節形式命題： Skolem標準形
(∀x1) (∀x2) ・・ (∀xn)[C1∧C2 ∧ ・・∧Cm]
[]内： 母式(matrix)
8
融合法（背理法）の原理
対象領域D, 論理式M[x]に対し，
∀ｘ [M[x]]が真であることを示すのは困難
一方，
∃a∈Dに対し， M[a]が偽であることを示せば
恒偽式であることは示せる
9
節形式への変換-1
冠頭標準形：論理式F:
(Q1x1)・・・(Qnxn)α
(Q1x1)・・・(Qnxn)：冠頭部 α：本体 Qi:束縛子
P → Qを￢P∨Qに、
Ａ≡Ｂを（ ￢Ａ∨Ｂ）∧（ ￢Ｂ∨Ａ）に変換
否定記号の括り出し： ￢（￢Ａ）=Ａ
￢（Ａ∧Ｂ）= （ ￢Ａ∨￢Ｂ）
￢（Ａ∨Ｂ）= （ ￢Ａ∧￢Ｂ）
￢ ((∀x)α）= (∃x)(￢α)
￢ ((∃x)α）= (∀x)(￢α)
10
節形式への変換 -2
Skolem標準形への変換
連言標準形へ変換
存在記号∃の除去：
(∀x) (∃y)P(x,y) = (∀x) P(x, f(x))
f(x): Skolem関数
存在記号を含む変数を引数とする新しい関数
で置き換えたもの
11
Skolem標準形への変換 例
∀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))∨Q(x1))∧((P(y2)∧R(y2) ∨￢R(g(y2)))]
存在記号∃の除去
12
節形式への変換 -3
1.
分配法則を用いて、母式を
選言の連言結合形に変換：
（Ａ∧Ｂ）∨（Ｂ∧C）=（Ａ∨Ｂ）∧ （Ｂ∨C）∧Ｂ∧（Ａ∨C）
P∨（Q∧R）=（P∨Q）∧（P∨R）
P∧（Q ∨ R）=（P∧Q）∨（P∧R）
２．節集合への変換：
P ∨ Q ∨ ￢ R ⇒ {P, Q, ￢ R}
（Ａ∨Ｂ）∧ （Ｂ∨C）∧Ｂ∧（Ａ∨C） ⇒
{{A,B}, {B,C}, {B}, {A,C}}
13
融合法による推論-１
代入(substitution)
以下の形式の有限集合：
{t1/v1, ・・・, tn/vn}
～ 互いに異なる変数viを各々，
項tiで置換える操作
14
融合法による推論-2
単一化(unification)
複数のリテラルの変数に適当な項を代入するこ
とにより、全てのリテラルを同一化すること
例）P(y, f(x))とP(a,z)の単一化
ｓ１=a/y: P(y, f(x)) ⇒ P(a, f(x)), P(a,z)不変
ｓ2=f(x)/z: P(a, z) ⇒ P(a, f(x)) で一致
15
融合法による推論-３
（２項）融合節(substitution)
共通変数を持たない節C1 , C２の
各々のリテラルL1 , L２で，
代入σによりL1 と ￢L２が単一化できるとき，
(C1 σ- L1 σ)∪(C2 σ- L2 σ)
例） C1 ＝{P(x),Q(x)} C2 ＝{￢P(a),R(y)}
の2項融合節は{Q(a),R(y)}
16
融合法による推論-４
導出原理(resolution principle)
目標の否定を前提に加えた節の集合から
導出・単一化を繰り返すことにより、矛盾
（空節）を導くこと
～ 節集合の充足不能性
17
融合法による推論例
前提S： A(x, b, c)∨B(x)
￢A(g(a), y, z)
￢B(v)∨ C(y, f(u))
目標： C(b, f(h(y)))
[推論方法]
目標の否定￢C(b, f(h(y)))を前提Ｓに加えて
ＮＩＬを導出
～ 一通りとは限らない
18
融合法による推論の例(結果）
P∧￢P＝空
19
証明の制御 -1
節の数が多い場合，効率良い導出のために，
どの親節を優先して選択するかの戦略が
重要
１．機械的戦略
線形導出：
必ず一方の親は入力節に所属 ～完全
幅優先戦略：
最初に入力節を親とする導出節を全て求め，
順次深いレベルから求めていく ～完全
20
証明の制御 -2
２．論理式の意味に基づく戦略
支持集合戦略：
少なくとも片方の親を支持集合，または支持集
合から導出された節から採る ～完全
支持集合T: 節集合C=H ∨ Tの時，
C：充足不能， H ：充足可能のとき
深さ優先戦略：
最初に目標命題の否定を１つの親とする導出を
１回行い，以後は直前に得られた導出節を親と
する導出を反復 ～不完全
21
証明の制御 例
前提： ￢R(u)∨P(u, v)
￢Q(w, z)∨S(z)
R(a)
￢S(b)
目標の否定：￢P(x, y)∨Q(x, y)
22
証明の制御 解法例
支持集合：￢P(x, y)∨Q(x, y)
23
© Copyright 2024 ExpyDoc
