转换为幻灯片


Start

XX

SMS 11011100XX

XX at gmail


背景

背景

  1. 人工智能-> 常识推理形式化
    thinking/acting humanly/rationally
  2. 常识推理的特点
    • 众多的例外

      “鸟会飞”:企鹅、鸵鸟、幼鸟、死鸟、玩具鸟等一干群众泪奔中。

    • 对环境的依存性

      “常在河边走,哪能不湿鞋”:表达的是一种经验。


对比数学和物理定律。

为形式地表述常识,并在常识间进行有效的形式推理,20世纪70年代人们提出了非单调逻辑


单调性与非单调性

单调性

逻辑系统 FS 是单调的, 如果对 FS 的任意公式集合 Γ1, Γ2, Γ1 ⊆ Γ2 蕴涵Th(Γ1)⊆Th(Γ2). 其中Th(Γ)表示Γ的演绎结果集合{A|ΓFSA}.

  • 之前讨论的所有逻辑 都是单调的 包括包含不一致的情况。

  • 但是常识推理不具有单调性a 会飞吗?;a 是鸟->会;a 是鸵鸟->不会

  • 常识推理的这种特性称为非单调性(与单调性的定义对应)

逻辑系统 FS 是非单调的, 如果存在公式集合Γ1, Γ2, Γ1 ⊊ Γ2Th(Γ1)⊈Th(Γ2).

  • 具有非单调性的推理称为非单调推理, 使用非单调推理的逻辑系统称为 非单调逻辑 在不完全的知识上推理

非单调逻辑的产生

非单调逻辑的产生

  • 封闭世界假设/ PLANNER 系统

    缺点: 需要保证可判定性/小心循环论证!

  • 用逻辑演算刻划状态转移

    STRIPS 系统

    • 一个动作的描述分为三部分:Action, Precondition, Effect
    • 添加表和删除表指 Effect 中的正文字和负文字。
    • 书上的例子

几种非单调逻辑系统

  1. 赖特(Reiter)的缺席推理逻辑

  2. 麦克德莫特(McDermott)和多伊尔(Doyle)的非单调逻辑系统

  3. 麦卡锡(McCarthy)的限定理论

缺席推理逻辑

  1. 已知鸟会飞,但只有鸵鸟不会飞
  2. 据说企鹅是鸟,得出企鹅会飞
  3. 又知道企鹅不会飞,不再推出企鹅会飞

形式规则


$$\frac{Bird(x):Mfly(x)}{fly(x)}$$


缺席推理规则的一般形式


$$\frac{\alpha(\vec x):M\beta_1(\vec x),\dots,M\beta_m(\vec x)}{w(\vec x)}$$

  • $\alpha(\vec x)$: 先决条件
  • $\beta_i(\vec x)$: 缺席条件
  • $w(\vec x)$: 结论
  • M: 常读作可能, $M\beta_i(\vec x)$表示就现有知识而言$\beta_i(\vec x)$可能成立, 即$\lnot\beta_i(\vec x)$尚未出现(缺席)。

如果缺席规则中不含自由变元,则称该规则为闭规则

缺席理论的定义

一个缺席推理逻辑理论(简称缺席理论或理论)由以下两部分组成:

  1. 缺席推理规则集 D;
  2. 公式集 W,它是已知的或约定的事实集合。

缺席理论常用二元矢<D, W> 表示。 当 D 中所有规则是闭规则时,称理论<D, W>闭理论

缺席理论是非单调的


缺席理论的“推出”

Δ = <D, W>是闭缺席理论,Γ关于 D 的一个算子Γ作用于任意命题集合 S, 其值为满足下列三个性质的最小命题集合Γ(S)

  • W ⊆ Γ(S)已知事实均成立。
  • Th(Γ(S)) = Γ(S), 这里的Th(Γ(S))为命题集{A|Γ(S)⊢FSFCA} 在经典逻辑的推出下封闭。
  • 若 D 中有规则$\frac{\alpha:M\beta_1,\dots,M\beta_m}{w}$, 且α ∈ Γ(S),¬β1, …, ¬βm ∉ S, 则w ∈ Γ(S). 包含缺席规则获得的知识。

命题集合E成为关于 D 的算子Γ固定点(fixed points),如果Γ(E)=E. 此时又称 E 为Δ = <D, W>的一个扩充


如果命题 A 包含在缺席理论Δ的一个扩充中,那么称 A 在Δ中可推出,记为 $\sdash_\Delta$ 表示非单调推出


缺席理论的扩充的性质

并非所有缺席理论都有扩充,并非有扩充的缺席理论只有惟一的扩充。 参考书上的三个例子。

  • 无扩充
    $D=\{\frac{:MA}{\lnot A}\}, W=\emptyset$
  • 唯一扩充
    $D=\{\frac{:MA}{\lnot B},\frac{:MB}{\lnot C},\frac{:MC}{\lnot F}\}, W=\emptyset$
    E = Th({¬B, ¬F})
  • 多个扩充
    $D=\{\frac{:MA}{A},\frac{B:MC}{C},\frac{F\lor A:ME}{E},\frac{C\land E:M\lnot A,M(F\lor A)}{G}\}$, W = {B, C → F ∨ A, A ∧ C → ¬E}
    E1 = Th(W ∪ {A, C}), E2 = Th(W ∪ {A, E}), E3 = Th(W ∪ {C, E, G})

设 E 为一阶命题集,Δ = <D, W>为一闭的缺席理论。 递归定义Ei(i = 1, 2, ⋯)如下:
E0 = W

$$E_{i+1}=Th(E_i)\cup\{w|\frac{\alpha:M\beta_1,\dots,M\beta_m}{w}\in D, \alpha\in E_i,\lnot\beta_1,\dots,\lnot\beta_m\not\in E\}$$

则 E 为Δ的一个扩充当且仅当$E=\bigcup_{i=0}^{\infty}E_i$.

闭缺席理论Δ = <D, W>有不一致扩充 E, 当且仅当W不一致。

Δ1 = <D1, W1>, Δ2 = <D2, W2>均为缺席理论, 且W1 ⊆ W2. 若Δ2的扩充都是一致的,则Δ1的扩充也是一致的。

设 E, F 为闭缺席理论Δ = <D, W>的两个扩充, 如果E ⊆ F, 则E = F.


规范缺席推理

一个缺席理论Δ = <D, W>称为是规范的,如果 D 中缺席规则均为 如下形式: 和封闭世界假设的关联
$$\frac{\alpha(\vec x):M w(\vec x)}{w(\vec x)}$$

它们被称为规范(缺席推理)规则。

闭规范缺席理论有很多漂亮的结果:

  • 闭规范缺席理论总有扩充。
  • 如果 E, F 同为一闭规范缺席理论的扩充,且 $E\neq F$,则 $E\cup F$ 是不一致的。
  • 设 $\Delta=\lt D,W\gt$ 为闭规范缺席理论,$D'\subseteq D$, 且 $E'_1$ 和 $E'_2$ 为 $\lt D',W\gt$ 的 两个不同扩充 只谈一个扩充 $E'_1$, 如下的$E_1$也是存在的。这里强调的是扩充的数量的单调性。 ,则 $\Delta$ 必有不同扩充 $E_1$ 和 $E_2$, 使 $E'_1\subseteq E_1, E'_2\subseteq E_2$.

闭规范缺席理论的扩充的大小,随闭规范缺席规则数目的增加而单调不减。


缺席理论的形式证明

Δ = <D, W> 为闭规范缺席理论,令
P(D)={α|αD中规则的先决条件}

C(D)={w|wD中规则的结论}

称一阶命题 βΔ 中的一个(缺席)证明, 如果存在 D 的有穷子集的有穷序列 D0, D1, …, Dk, 使得

  1. W ∪ C(D0)⊢FSFCβ.
  2. 对于整数 i, 1 ≤ i ≤ k, 及 P(Di − 1) 中每一个 α, W ∪ C(Di)⊢FSFCα.

    证明序列中前面的先决条件逐个被后头的结论支持。

  3. Dk = ϕ.
  4. $W\cup \bigcup_{i=0}^{k}{C(D_i)}$ 可满足。

缺席证明的消解方法

  1. 构造 S 包括所有 W 中的命题,待证命题否定的子句,以及所有规则的结果子句 $(c_i, \{\delta\})$, 其中 $\delta=\frac{\alpha:Mw}{w}\in D, c_i\textrm{是} w\textrm{的子句}$。
  2. 对 S 消解导出空子句。
  3. 消解过程中使用的结果子句所在的规则构成 $D_0$, 接下来继续消解证明 $D_0$ 中所有规则的先决条件,直到消解过程中不需要使用规则的结果子句,消解结束。

见书例11.6。


缺席推理的局限性

  1. 存在闭规范缺席理论是完全不可判定的。

    所以上面的消解算法不可能是完备的。

    尽管如此,上述方法仍然是有力的。

  2. 语义研究进展不足。


非单调逻辑

非单调逻辑

设理论 T 有以下三条公理:

  1. 正值中午 ∧ M(出太阳)→出太阳, 模态词 M 表示与当前已推得的定理相容。
  2. 正值中午
  3. 日食 → ¬()

则在 T 中可证

4. 出太阳

但若将

5. 日食

加入公理,则 4. 不再可证。

与缺席推理的不同: MA 的地位不同。


非单调逻辑系统

M的意义:
$$\textrm{如果}\not\vdash\lnot A, \textrm{则}~\sdash MA$$

将加入模态词 M 的一阶谓词演算系统记为 FC, 将允许使用 M 的一阶公式全体记为 $L_{FC}$, 对任何公式集 $\Gamma\subseteq L_{FC}$, $Th(\Gamma)=\{A|\Gamma\vdash_{FC}A\}$.

对任何公式集 Γ ⊆ LFC 定义算子 NMΓ, 对任意公式集 S ⊆ LFC


NMΓ(S)=Th(Γ ∪ AsΓ(S))

其中 AsΓ(S) 称为 S 的 假设集 与 S 相容的所有假设


AsΓ(S)={MQ|Q ∈ LFC ∧ ¬Q ∉ S}


TH(Γ)=⋂({LFC}∪{S|NMΓ(S)=S})

如果 P ∈ TH(Γ) 这里 C = {x|∀S(S ∈ C → x ∈ S)}. 即元素交。
即是说, TH(Γ) 表示的是 NMΓ所有固定点的交 NMΓ 的最小不动点 。 当 NMΓ 无固定点时, TH(Γ) 是全体 FC 公式。
, 那么称 P 可由 Γ 非单调地推出( 可证 与缺席推理理论不同,要求 P 在所有固定点中,后者只需某个 ), 并记为 $\Gamma\sdash P$.


示意图
示意图
关系示意图

非单调逻辑系统扩充的性质

与缺省逻辑里的 $\Gamma$ 算子一样, $NM_\Gamma$ 算子的固定点也未必存在,存在也未必唯一。

书上的一些例子:

  • Γ = FC ∪ {MC → ¬C}, NMΓ 没有固定点。
  • Γ = FC ∪ {A ∧ MB → B, C ∧ MD → D, A ∨ C}, NMΓ 有唯一固定点。
  • Γ = FC ∪ {MC → ¬D, MD → ¬C}, NMΓ 有两个固定点。

甚至可能有无穷个固定点。


非单调逻辑系统固定点的性质

Q1, Q2, Q3, ⋯, LFC 的一个枚举, Γ ⊆ LFC. 令


Γ0 = Γ

$$ \Gamma_{i+1} = \left\{\begin{array}{ll} L_{FC} &amp; \textrm{如果有} P\in L_{FC} \textrm{使} MP\in\Gamma_i \textrm{且} \Gamma_i\vdash\lnot P\\ \Gamma_i\cup\{MQ_i\} &amp; \textrm{如果}\Gamma_i\cup\{Q_i\}\textrm{一致}\\ \Gamma_i &amp; \textrm{否则}\\ \end{array}\right. $$

$\Gamma_\infty=\bigcup_{i=0}^\infty{\Gamma_i}$, 则 $\Gamma\sdash P$ 当且仅当对 LFC 的每一枚举,均有 ΓFCP.

存在 Γ′⊆Γ, NMΓ 有固定点,但 NMΓ 无固定点。 (对比定理 11.2)

如果 F1, F2 均为 NMΓ 的固定点,且 F1 ⊆ F2, 则 F1 = F2. (对比定理 11.3)

对应于闭规范缺席理论的非单调理论不一定有扩充。


非单调逻辑系统的形式证明

非单调命题逻辑的可证性是可判定的。但一般地,非单调逻辑的可证性是不可判定的。

下面的算法类似于命题演算的真值表方法。

  1. 要证 $\Gamma\sdash A$, 对使 $\Gamma\to A$ 假的一切可能情况列表。

  2. 表的第一列为 $\Gamma$ 中的公式,它们总取值为 1. 第二列为待证公式 A 的表,称为 t 表, A 总取值为 0,由 $\Gamma$ 和 A 的值计算子公式的真值。 当 t 中出现取值为 0 的 MB 形公式时,建立以 $\Gamma\to\lnot B$ 为目标的新表。

  3. 对表各分支如下标记(称为适当的) open 无法否证 B, 所以 MB 可以满足closed 矛盾,反证成功

    1. 当 $\Gamma\sdash \lnot B$ 的表标记open时,对每一表中的 MB 标记为 1.
    2. 表的分支标记为 closed 当且仅当该分支中有公式同时标记了 0 和 1. 一分支标记为 open 当且仅当该分支不能被标记为 closed.
  4. $\Gamma\to A$ 当且仅当在所有适当标记中,t 均被标记为 closed.

见书上的两个例子。


加贝的语义解释

加贝 (Gabbay) 对非单调逻辑作了 直觉主义的语义解释 “Hi, 小朋友们大家好,还记得我是谁吗?”——克里普克 P.103


$$\models_{\mathscr K}^k MA \textrm{当且仅当存在}l\geq k\textrm{使}\models_{\mathscr K}^l A$$


MA ∨ ¬A

⊨¬MA ↔ ¬A

⊨(MA → B)↔(¬A ∨ B)

⊨(MC → ¬C)↔¬C


加贝语义的非单调可证性

A, B ∈ LFC, B 由 A 非单调可证( $A\sdash B$ )指存在公式序列
C0 = A, C1, C2, ⋯, Cn = B
以及称为额外假设的公式
MX11, ⋯, MXk(1)1; MX12, ⋯, ⋯, MXk(2)2; ⋯; MX1n, ⋯, MXk(n)n
使得
$$C_{i-1}\land\bigwedge_{j=1}^{k(i)}MX_j^i\models C_i(i=1,2,\cdots,n)$$

如果 A ∧ MB ⊨ C 并且 C ∧ MD ⊨ E, 那么 $A\sdash C$, $C\sdash E$, 从而易证 $A\sdash E$, 因为
A, C, E

MB; MD
即为上面非单调可证需要的公式序列和额外假设公式。


加贝语义中的 $\sdash$ 对比 M & D 的定义中的 $\sdash$ 要更符合直观:

  • 加贝语义中有 $M(A\land B)\sdash MA$ 和 $\lnot MA\sdash\lnot A$
  • 加贝语义中 $MC\land\lnot C$ 不一致

但加贝的讨论局限于命题演算中。

TMS(真值维持系统):

  • 记录每条信念的依赖关系
  • 当新信念否定了旧信念时,回溯依赖关系消除不一致

限定逻辑

将已发现的具有某些性质的客体视为具有该性质的全部客体, 直至具有该性质的其它客体被发现时修改这一看法。

Idea: 奥卡姆剃刀(Occam principle)

麦卡锡并未引入新的算子或逻辑符号,只是在经典逻辑框架内研究适合表示非单调性的特殊推理形式。


限定

n 元谓词 P 在一阶公式 A(P) 中的限定是指如下的公式模式
$$A(\Phi)\land\forall\vec x(\Phi(\vec x)\to P(\vec x))\to\forall\vec x(P(\vec x)\to\Phi(\vec x))$$

A(Φ) 表示将 A 中所有 P 的出现替换为公式 Φ.

  • 想表达什么? 所谓对公式 A 的限定就是:
    如果用谓词 $\Phi$ 满足 P 满足的条件( A ), 并且满足 $\Phi$ 的客体都满足 P, 则满足 P 的客体都满足 $\Phi$ 。

见书上例子:方块世界和数学归纳法。


域限定

假设个体域为 $\{x|P(x)\}$, 则任意公式 A 中的量词可如下改变,A 的意义不变:

  • A 中的 $\exists x B(x)$, 可改为 $\exists x(P(x)\land B(x))$.
  • A 中的 $\forall x B(x)$, 可改为 $\forall x(P(x)\to B(x))$.

公式 A 的域限定指对 A 中 P 作限定,即


AΦ → ∀xΦ(x)

其中 $A^\Phi$ 表示将 A 中 $\exists x B(x)$ 改为 $\exists x(\Phi(x)\land B(x))$, $\forall x C(x)$ 改为 $\forall x(\Phi(x)\to C(x))$ 后所得的公式。

意义:若 A 在论域 $\{x|\Phi(x)\}$ 中为真,则所有满足 A 的个体都满足 $\Phi(x)$.

令 B(x) 表示 x 是渡河工具,Φ(x) 表示 x 是船。 A 为 xB(x). 对 A 用 Φ(x) 做限定,得
x(Φ(x)→B(x)) → ∀xΦ(x)
由于 Φ(x)→B(x) 为真,故 xΦ(x) 为真,即所有渡河工具都是船。


限定论可证

对任意公式 A, 令 Ω(A)={[AΦ → ∀xΦ(x)]0|Φ为任一含自由变元x的一阶公式}. 这里 B0表示 B 的全称封闭式。又令
MC(A)=Ω(A)∪{A},
MC(A) 称为 A 的最小完备集

如果 MC(A)⊢FSFCB, 则称一阶公式 B 由一阶公式 A 限定论可证,记为 $A\sdash_{mc}B$.

限定一阶语言仅含一个一元谓词 P(x), 有 $\exists x P(x)\sdash_{mc}\forall x P(x)$.

限定论可证的非单调性:当限定被取消或改变时。


限定理论的语义

Γ 为一阶命题集,称结构 𝔄 = <U, I>Γ最小模型, 如果

  • 对每个 A ∈ Γ, ⊨𝔄A.
  • 𝒰 的任一子结构 𝔄′= < U′,I′>(U′⊂U, I′=IU, IU 表示将解释 I 限于 U, 例如对一元谓词 P, IU(P)=I(P)∩U′) 存在 A ∈ Γ, 使 $\not\models_{\mathfrak{A}'} A$.

称一阶命题 B 为一阶命题集 Γ最小逻辑结果, 记为 ΓmcB, 如果 B 在所有 Γ 的最小模型中均真。

见书上例子。


Γ1 = ∅, 其最小模型为所有个体域为幺元集的结构, 有
Γ1mcxy(x = y)
.

Γ2 = {∃xy(x ≠ y)}, 其最小模型为所有个体域含有两个元素的结构, 有
$$\Gamma_2\not\models_{mc}\forall x\forall y(x=y)$$
.

上面例子说明 $\models_{mc}$ 不是单调的。


限定可证性的合理性和完备性

对任何一阶命题 A, B, 如果 $A\sdash_{mc} B$, 则 AmcB.

𝔄 = <U, I> 为 A 的最小模型,C 为 Ω(A) 中的任一公式。 先证 𝔄C.

只需证 𝔄[AΦ → ∀xΦ(x)]0. 将论域限定到满足 Φ 的个体集上即可。

再证 AmcB. 将 $\sdash_{mc}$ 转化到 FSFC上即可。

限定可证性不具有完备性。

考虑例 11.18.


性质限定

“船可以渡河”:

  • 域限定:只有船可以渡河
  • 性质限定:船只能渡河

$A(\vec P)$ 为一二阶公式, $\vec P$ 为一组谓词变元 P0, …, Pn 的缩写。 又设 $E(\vec P, \vec x)$ 是含自由谓词变元 P0, …, Pn 和个体变元 x1, …, xm 的二阶公式。称下列二阶公式为 $E(\vec P, \vec x)$ 关于 $A(\vec P)$性质限定

$A(\vec P)\land\forall\vec{P'}(A(\vec{P'})\land\forall{\vec x}(E(\vec{P'}, \vec x)\to E(\vec P, \vec x))\to\forall \vec x(E(\vec{P'},\vec x)\leftrightarrow E(\vec P, \vec x)))$ 对比限定的原始形式:$A(\Phi)\land\forall\vec x(\Phi(\vec x)\to P(\vec x))\to\forall\vec x(P(\vec x)\to\Phi(\vec x))$  口

令 E(Q, x) 表示 “x 具有性质 Q”,P 表示“能渡河”的性质,A(Q) 表示“Q 是船的性质”, 若接受 A(P),则 E(Q, x) 关于 A(P) 的性质限定为:

P′(A(P′) ∧ ∀x(E(P′,x)→E(P, x)) → ∀x(E(P′,x)↔E(P, x))) 如果一个船的性质是“能渡河”的子属性,则这个性质就是“能渡河”。


性质限定(续)

$A(\vec P), \vec P$ 的意义同定义 11.15,称下列二阶公式为 A 中 谓词变元 P0 具有 P1, ⋯, Pn 的限定, 记为 Circum(A; P0, P1, ⋯, Pn)

$A(\vec P)\land \forall\vec{P'}(A(\vec{P'})\land\forall\vec{x}(P_0'(\vec x)\to P_0(x))\to\forall\vec x(P_0'(\vec x)\leftrightarrow P_0(\vec x)))$ 继续对比限定的原始形式:$A(\Phi)\land\forall\vec x(\Phi(\vec x)\to P(\vec x))\to\forall\vec x(P(\vec x)\to\Phi(\vec x))$  口

A(D, L) 表示如下事实:
x(Dx ↔ ¬Lx)∧La ∧ Db ∧ Rc ∧ (a ≠ b ∧ a ≠ c ∧ b ≠ c)
其中 Dx 表示 x 死了, Lx 表示 x 活着,Rx 表示 x 是兔子, 想要限定“全部死了的客体就是已知死了的客体(即 b)”。 只用之前的限定方法限定 D,由于无法推出 ¬Dc(Lc),无法得到我们想要的结果。 用性质限定,得到
$$\forall x(P_0(x)\leftrightarrow\lnot P_1(x))\land P_1(a)\land P_0(b)\land Rc\land (a\neq b\land a\neq c\land b\neq c)\land \forall x(P_0(x)\to Dx)\\ \to\forall x(P_0(x)\leftrightarrow Dx)$$
P0(x)x = b, P1(x)x ≠ b,即得
x(x = b ↔ Dx)
即得我们想要的结果。


性质限定的可满足性

如果 $A(P)$ 的限定是可满足的,那么 $A(P)$ 也是可满足的,但反之不然。

见书上例 11.21

如果 $A(\vec P)$ 为一可满足的 全称命题 前束范式中不含存在量词 ,那么 $Circum(A(\vec P), \vec P)$ 也是可满足的。


限定理论的应用前景

Frame problem: 在动作后状态的改变只局限在动作影响到的部分上。


Thank you!


comments powered by Disqus