非单调逻辑
Start
XX
SMS 11011100XX
XX at gmail
背景
背景
- 常识推理的特点
众多的例外
“鸟会飞”：企鹅、鸵鸟、幼鸟、死鸟、玩具鸟等一干群众泪奔中。
对环境的依存性
“常在河边走，哪能不湿鞋”：表达的是一种经验。
对比数学和物理定律。
为形式地表述常识，并在常识间进行有效的形式推理，20世纪70年代人们提出了非单调逻辑。
单调性与非单调性
单调性
逻辑系统 FS 是单调的， 如果对 FS 的任意公式集合 Γ1, Γ2, Γ1 ⊆ Γ2 蕴涵Th(Γ1)⊆Th(Γ2). 其中Th(Γ)表示Γ的演绎结果集合{A|Γ⊢FSA}.
之前讨论的所有逻辑
但是a 会飞吗？；a 是鸟->会；a 是鸵鸟->不会
常识推理的这种特性称为非单调性(与单调性的定义对应)
逻辑系统 FS 是非单调的, 如果存在公式集合Γ1, Γ2, Γ1 ⊊ Γ2 但Th(Γ1)⊈Th(Γ2).
- 具有非单调性的推理称为非单调推理, 使用非单调推理的逻辑系统称为
非单调逻辑的产生
非单调逻辑的产生
封闭世界假设/ PLANNER 系统
缺点: 需要保证可判定性/小心循环论证！
用逻辑演算刻划状态转移
STRIPS 系统
- 一个动作的描述分为三部分：Action, Precondition, Effect
- 添加表和删除表指 Effect 中的正文字和负文字。
- 书上的例子
几种非单调逻辑系统
赖特(Reiter)的缺席推理逻辑
麦克德莫特(McDermott)和多伊尔(Doyle)的非单调逻辑系统
麦卡锡(McCarthy)的限定理论
缺席推理逻辑
- 已知鸟会飞，但只有鸵鸟不会飞
- 据说企鹅是鸟，得出企鹅会飞
- 又知道企鹅不会飞，不再推出企鹅会飞
形式规则
$$\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)$尚未出现(缺席)。
如果缺席规则中不含自由变元，则称该规则为闭规则。
缺席理论的定义
一个缺席推理逻辑理论(简称缺席理论或理论)由以下两部分组成：
- 缺席推理规则集 D;
- 公式集 W，它是已知的或约定的事实集合。
缺席理论常用二元矢<D, W> 表示。 当 D 中所有规则是闭规则时，称理论<D, W>为闭理论。
缺席理论是非单调的。
缺席理论的“推出”
设 Δ = <D, W>是闭缺席理论，Γ为关于 D 的一个算子， Γ作用于任意命题集合 S, 其值为满足下列三个性质的最小命题集合Γ(S)：
命题集合E成为关于 D 的算子Γ的固定点(fixed points)，如果Γ(E)=E. 此时又称 E 为Δ = <D, W>的一个扩充。
如果命题 A 包含在缺席理论Δ的一个扩充中，那么称 A 在Δ中可推出，记为
缺席理论的扩充的性质
并非所有缺席理论都有扩充，并非有扩充的缺席理论只有惟一的扩充。 参考书上的三个例子。
-
无扩充
$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$ 的 ，则 $\Delta$ 必有不同扩充 $E_1$ 和 $E_2$， 使 $E'_1\subseteq E_1, E'_2\subseteq E_2$.
闭规范缺席理论的扩充的大小，随闭规范缺席规则数目的增加而单调不减。
缺席理论的形式证明
设 Δ = <D, W> 为闭规范缺席理论，令
P(D)={α|α为D中规则的先决条件}
C(D)={w|w为D中规则的结论}
称一阶命题 β 有 Δ 中的一个(缺席)证明， 如果存在 D 的有穷子集的有穷序列 D0, D1, …, Dk, 使得
- W ∪ C(D0)⊢FSFCβ.
-
对于整数 i, 1 ≤ i ≤ k, 及 P(Di − 1) 中每一个 α, W ∪ C(Di)⊢FSFCα.
证明序列中前面的先决条件逐个被后头的结论支持。
- Dk = ϕ.
- $W\cup \bigcup_{i=0}^{k}{C(D_i)}$ 可满足。
缺席证明的消解方法
- 构造 S 包括所有 W 中的命题，待证命题否定的子句，以及所有规则的结果子句 $(c_i, \{\delta\})$, 其中 $\delta=\frac{\alpha:Mw}{w}\in D, c_i\textrm{是} w\textrm{的子句}$。
- 对 S 消解导出空子句。
- 消解过程中使用的结果子句所在的规则构成 $D_0$, 接下来继续消解证明 $D_0$ 中所有规则的先决条件，直到消解过程中不需要使用规则的结果子句，消解结束。
见书例11.6。
缺席推理的局限性
存在闭规范缺席理论是完全不可判定的。
所以上面的消解算法不可能是完备的。
尽管如此，上述方法仍然是有力的。
语义研究进展不足。
非单调逻辑
非单调逻辑
设理论 T 有以下三条公理：
- 正值中午 ∧ M(出太阳)→出太阳, 模态词 M 表示与当前已推得的定理相容。
- 正值中午
- 日食 → ¬(出太阳)
则在 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 的 。
AsΓ(S)={MQ|Q ∈ LFC ∧ ¬Q ∉ S}
令
TH(Γ)=⋂({LFC}∪{S|NMΓ(S)=S})
如果 , 那么称 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} & \textrm{如果有} P\in L_{FC}
\textrm{使} MP\in\Gamma_i \textrm{且} \Gamma_i\vdash\lnot P\\
\Gamma_i\cup\{MQ_i\} & \textrm{如果}\Gamma_i\cup\{Q_i\}\textrm{一致}\\
\Gamma_i & \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)
对应于闭规范缺席理论的非单调理论不一定有扩充。
非单调逻辑系统的形式证明
非单调命题逻辑的可证性是可判定的。但一般地，非单调逻辑的可证性是不可判定的。
下面的算法类似于命题演算的真值表方法。
要证 $\Gamma\sdash A$, 对使 $\Gamma\to A$ 假的一切可能情况列表。
表的第一列为 $\Gamma$ 中的公式，它们总取值为 1. 第二列为待证公式 A 的表，称为 t 表， A 总取值为 0，由 $\Gamma$ 和 A 的值计算子公式的真值。 当 t 中出现取值为 0 的 MB 形公式时，建立以 $\Gamma\to\lnot B$ 为目标的新表。
对表各分支如下标记(称为适当的) 或 ：
- 当 $\Gamma\sdash \lnot B$ 的表标记open时，对每一表中的 MB 标记为 1.
- 表的分支标记为 closed 当且仅当该分支中有公式同时标记了 0 和 1. 一分支标记为 open 当且仅当该分支不能被标记为 closed.
$\Gamma\to A$ 当且仅当在所有适当标记中，t 均被标记为 closed.
见书上的两个例子。
加贝的语义解释
加贝 (Gabbay) 对非单调逻辑作了 ：
$$\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 的出现替换为公式 Φ.
见书上例子：方块世界和数学归纳法。
域限定
假设个体域为 $\{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′=I∣U′, I∣U′ 表示将解释 I 限于 U′, 例如对一元谓词 P, I∣U′(P)=I(P)∩U′) 存在 A ∈ Γ, 使 $\not\models_{\mathfrak{A}'} A$.
称一阶命题 B 为一阶命题集 Γ 的最小逻辑结果, 记为 Γ⊨mcB, 如果 B 在所有 Γ 的最小模型中均真。
见书上例子。
Γ1 = ∅, 其最小模型为所有个体域为幺元集的结构， 有
Γ1⊨mc∀x∀y(x = y)
.
Γ2 = {∃x∃y(x ≠ y)}, 其最小模型为所有个体域含有两个元素的结构， 有
$$\Gamma_2\not\models_{mc}\forall x\forall y(x=y)$$
.
上面例子说明 $\models_{mc}$ 不是单调的。
限定可证性的合理性和完备性
对任何一阶命题 A, B, 如果 $A\sdash_{mc} B$, 则 A⊨mcB.
设 𝔄 = <U, I> 为 A 的最小模型，C 为 Ω(A) 中的任一公式。 先证 ⊨𝔄C.
只需证 ⊨𝔄[AΦ → ∀xΦ(x)]0. 将论域限定到满足 Φ 的个体集上即可。
再证 A⊨mcB. 将 $\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)$ 的性质限定：
令 E(Q, x) 表示 “x 具有性质 Q”，P 表示“能渡河”的性质，A(Q) 表示“Q 是船的性质”， 若接受 A(P)，则 E(Q, x) 关于 A(P) 的性质限定为：
性质限定(续)
$A(\vec P), \vec P$ 的意义同定义 11.15,称下列二阶公式为 A 中 谓词变元 P0 具有 P1, ⋯, Pn 的限定， 记为 Circum(A; P0, P1, ⋯, Pn)：
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: 在动作后状态的改变只局限在动作影响到的部分上。