XX
SMS 11011100XX
XX at gmail
背景
-
人工智能
thinking/acting humanly/rationally
-> 常识推理形式化
-
常识推理的特点
-
众多的例外
“鸟会飞”：企鹅、鸵鸟、幼鸟、死鸟、玩具鸟等一干群众泪奔中。
-
对环境的依存性
“常在河边走，哪能不湿鞋”：表达的是一种经验。
对比数学和物理定律。
为形式地表述常识，并在常识间进行有效的形式推理，20世纪70年代人们提出了非单调逻辑。
单调性与非单调性
单调性
逻辑系统 FS 是单调的，
如果对 FS 的任意公式集合
\(\Gamma_1, \Gamma_2\),
\(\Gamma_1\subseteq\Gamma_2\)
蕴涵 \(Th(\Gamma_1)\subseteq Th(\Gamma_2)\).
其中 \(Th(\Gamma)\) 表示 \(\Gamma\) 的演绎结果集合 \(\{A|\Gamma\vdash_{FS} A\}\).
-
之前讨论的所有逻辑
都是单调的
包括包含不一致的情况。
-
但是
常识推理不具有单调性
a 会飞吗？
a 是鸟->会
a 是鸵鸟->不会
-
常识推理的这种特性称为非单调性(与单调性的定义对应)
逻辑系统 FS 是非单调的,
如果存在公式集合 \(\Gamma_1, \Gamma_2\),
\(\Gamma_1\subsetneq\Gamma_2\)
但 \(Th(\Gamma_1)\nsubseteq Th(\Gamma_2)\).
-
具有非单调性的推理称为非单调推理, 使用非单调推理的逻辑系统称为
非单调逻辑
在不完全的知识上推理
非单调逻辑的产生
-
封闭世界假设/ PLANNER 系统
缺点:
需要保证可判定性/小心循环论证！
-
用逻辑演算刻划状态转移
STRIPS 系统
- 一个动作的描述分为三部分：Action, Precondition, Effect
- 添加表和删除表指 Effect 中的正文字和负文字。
- 书上的例子
几种非单调逻辑系统
-
赖特(Reiter)的缺席推理逻辑
-
麦克德莫特(McDermott)和多伊尔(Doyle)的非单调逻辑系统
-
麦卡锡(McCarthy)的限定理论
缺席推理逻辑
- 已知鸟会飞，但只有鸵鸟不会飞
- 据说企鹅是鸟，得出企鹅会飞
- 又知道企鹅不会飞，不再推出企鹅会飞
形式规则
缺席推理规则的一般形式
- \(\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 中所有规则是闭规则时，称理论 为闭理论。
缺席理论是非单调的。
缺席理论的“推出”
设 \(\Delta=\lt D, W\gt\) 是闭缺席理论，\(\Gamma\) 为关于 D 的一个算子，
\(\Gamma\) 作用于任意命题集合 S, 其值为满足下列三个性质的最小命题集合 \(\Gamma(S)\)：
-
\(W\subseteq\Gamma(S)\)
已知事实均成立。
-
\(Th(\Gamma(S))=\Gamma(S)\), 这里的 \(Th(\Gamma(S))\) 为命题集 \(\{A|\Gamma(S)\vdash_{FSFC}A\}\)
在经典逻辑的推出下封闭。
-
若 D 中有规则\(\frac{\alpha:M\beta_1,\dots,M\beta_m}{w}\)，
且 \(\alpha\in\Gamma(S), \lnot\beta_1,\dots,\lnot\beta_m\not\in S\)，
则 \(w\in\Gamma(S)\).
包含缺席规则获得的知识。
命题集合E成为关于 D 的算子 \(\Gamma\) 的固定点(fixed points)，如果 \(\Gamma(E)=E\).
此时又称 E 为 \(\Delta=\lt D, W\gt\) 的一个扩充。
如果命题 A 包含在缺席理论 \(\Delta\) 的一个扩充中，那么称 A 在 \(\Delta\) 中可推出，记为
\(\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(\{\lnot B, \lnot 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\to F\lor A, A\land C\to\lnot E\}\)
\(E_1 = Th(W\cup\{A, C\}),E_2 = Th(W\cup\{A, E\}),E_3 = Th(W\cup\{C, E, G\})\)
设 E 为一阶命题集，\(\Delta=\lt D,W\gt\) 为一闭的缺席理论。
递归定义 \(E_i(i=1,2,\cdots)\) 如下：
$$E_0=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 为 \(\Delta\) 的一个扩充当且仅当 \(E=\bigcup_{i=0}^{\infty}E_i\).
闭缺席理论 \(\Delta=\lt D,W\gt\) 有不一致扩充 E, 当且仅当W不一致。
设 \(\Delta_1=\lt D_1,W_1\gt\), \(\Delta_2=\lt D_2,W_2\gt\) 均为缺席理论，
且 \(W_1\subseteq W_2\). 若 \(\Delta_2\) 的扩充都是一致的，则 \(\Delta_1\) 的扩充也是一致的。
设 E, F 为闭缺席理论 \(\Delta=\lt D,W\gt\) 的两个扩充，
如果 \(E\subseteq F\), 则 \(E=F\).
规范缺席推理
一个缺席理论 \(\Delta=\lt D,W\gt\) 称为是规范的，如果 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\).
闭规范缺席理论的扩充的大小，随闭规范缺席规则数目的增加而单调不减。
缺席理论的形式证明
设 \(\Delta=\lt D,W\gt\) 为闭规范缺席理论，令
$$P(D)=\{\alpha|\alpha\textrm{为}D\textrm{中规则的先决条件}\}$$
$$C(D)=\{w|w\textrm{为}D\textrm{中规则的结论}\}$$
称一阶命题 \(\beta\) 有 \(\Delta\) 中的一个(缺席)
证明，
如果存在 D 的有穷子集的有穷序列 \(D_0,D_1,\dots,D_k\), 使得
-
\(W\cup C(D_0)\vdash_{FSFC} \beta\).
-
对于整数 \(i\), \(1\leq i \leq k\), 及 \(P(D_{i-1})\) 中每一个 \(\alpha\),
\(W\cup C(D_i)\vdash_{FSFC}\alpha\).
证明序列中前面的先决条件逐个被后头的结论支持。
-
\(D_k=\phi\).
-
\(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 有以下三条公理：
-
\(\textrm{正值中午}\land M(\textrm{出太阳})\to\textrm{出太阳}\)
模态词 M 表示与当前已推得的定理相容。
-
正值中午
-
\(\textrm{日食}\to\lnot(出太阳)\)
则在 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\}\).
对任何公式集 \(\Gamma\subseteq L_{FC}\) 定义算子 \(NM_\Gamma\),
对任意公式集 \(S\subseteq L_{FC}\)
$$NM_\Gamma(S)=Th(\Gamma\cup A_{s_\Gamma}(S))$$
其中 \(A_{s_\Gamma}(S)\) 称为 S 的
假设集
与 S 相容的所有假设
。
$$A_{s_\Gamma}(S)=\{MQ|Q\in L_{FC}\land \lnot Q\not\in S\}$$
令
$$TH(\Gamma)=\bigcap(\{L_{FC}\}\cup\{S|NM_\Gamma(S)=S\})$$
如果
\(P\in TH(\Gamma)\)
这里 \(\bigcap C=\{x|\forall S(S\in C\to x\in S)\}\). 即元素交。
即是说， \(TH(\Gamma)\) 表示的是 \(NM_\Gamma\) 的
所有固定点的交
\(NM_\Gamma\) 的最小不动点
。
当 \(NM_\Gamma\) 无固定点时， \(TH(\Gamma)\) 是全体 FC 公式。
, 那么称 P 可由 \(\Gamma\) 非单调地推出(
可证
与缺席推理理论不同，要求 P 在所有固定点中，后者只需某个。
)，
并记为 \(\Gamma\sdash P\).
关系示意图
非单调逻辑系统扩充的性质
与缺省逻辑里的 \(\Gamma\) 算子一样， \(NM_\Gamma\) 算子的固定点也未必存在，存在也未必唯一。
书上的一些例子：
-
\(\Gamma=FC\cup\{MC\to\lnot C\}\), \(NM_\Gamma\) 没有固定点。
-
\(\Gamma=FC\cup\{A\land MB\to B, C\land MD\to D, A\lor C\}\), \(NM_\Gamma\) 有唯一固定点。
-
\(\Gamma=FC\cup\{MC\to\lnot D, MD\to\lnot C\}\), \(NM_\Gamma\) 有两个固定点。
甚至可能有无穷个固定点。
非单调逻辑系统固定点的性质
设 \(Q_1,Q_2,Q_3,\cdots,\) 是 \(L_{FC}\) 的一个枚举，
\(\Gamma\subseteq L_{FC}\). 令
$$\Gamma_0 = \Gamma$$
$$
\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\) 当且仅当对 \(L_{FC}\) 的每一枚举，均有
\(\Gamma_\infty\vdash_{FC}P\).
存在 \(\Gamma'\subseteq\Gamma\), \(NM_\Gamma\) 有固定点，但 \(NM_{\Gamma'}\) 无固定点。
(对比定理 11.2)
如果 \(F_1, F_2\) 均为 \(NM_\Gamma\) 的固定点，且 \(F_1\subseteq F_2\),
则 \(F_1=F_2\).
(对比定理 11.3)
对应于闭规范缺席理论的非单调理论不一定有扩充。
非单调逻辑系统的形式证明
非单调命题逻辑的可证性是可判定的。但一般地，非单调逻辑的可证性是不可判定的。
下面的算法类似于命题演算的真值表方法。
-
要证 \(\Gamma\sdash A\), 对使 \(\Gamma\to A\) 假的一切可能情况列表。
-
表的第一列为 \(\Gamma\) 中的公式，它们总取值为 1.
第二列为待证公式 A 的表，称为 t 表，
A 总取值为 0，由 \(\Gamma\) 和 A 的值计算子公式的真值。
当 t 中出现取值为 0 的 MB 形公式时，建立以 \(\Gamma\to\lnot B\) 为目标的新表。
-
对表各分支如下标记(称为适当的)
open
无法否证 B, 所以 MB 可以满足
或
closed
矛盾，反证成功
：
- 当 \(\Gamma\sdash \lnot B\) 的表标记open时，对每一表中的 MB 标记为 1.
- 表的分支标记为 closed 当且仅当该分支中有公式同时标记了 0 和 1.
一分支标记为 open 当且仅当该分支不能被标记为 closed.
-
\(\Gamma\to A\) 当且仅当在所有适当标记中，t 均被标记为 closed.
见书上的两个例子。
加贝的语义解释
加贝 (Gabbay) 对非单调逻辑作了
直觉主义的语义解释
“Hi, 小朋友们大家好，还记得我是谁吗？”——克里普克 P.103
：
$$\models_{\mathscr K}^k MA \textrm{当且仅当存在}l\geq k\textrm{使}\models_{\mathscr K}^l A$$
$$\models MA \lor\lnot A$$
$$\models \lnot MA\leftrightarrow \lnot A$$
$$\models (MA\to B)\leftrightarrow(\lnot A\lor B)$$
$$\models (MC\to\lnot C)\leftrightarrow\lnot C$$
加贝语义的非单调可证性
设 \(A, B\in L_{FC}\), B 由 A 非单调可证( \(A\sdash B\) )指存在公式序列
$$C_0=A,C_1,C_2,\cdots,C_n=B$$
以及称为额外假设的公式
$$MX_1^1,\cdots,MX_{k(1)}^1;MX_1^2,\cdots,\cdots,MX_{k(2)}^2;\cdots;MX_1^n,\cdots,MX_{k(n)}^n$$
使得
$$C_{i-1}\land\bigwedge_{j=1}^{k(i)}MX_j^i\models C_i(i=1,2,\cdots,n)$$
如果 \(A\land MB\models C\) 并且 \(C\land MD\models 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(\Phi)\) 表示将 A 中所有 P 的出现替换为公式 \(\Phi\).
- 想表达什么？
所谓对公式 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^\Phi\to\forall x\Phi(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 是渡河工具，\(\Phi(x)\) 表示 x 是船。
A 为 \(\forall x B(x)\).
对 A 用 \(\Phi(x)\) 做限定，得
$$\forall x(\Phi(x)\to B(x))\to \forall x\Phi(x)$$
由于 \(\Phi(x)\to B(x)\) 为真，故 \(\forall x\Phi(x)\) 为真，即所有渡河工具都是船。
限定论可证
对任意公式 A, 令 \(\Omega(A)=\{[A^\Phi\to\forall x\Phi(x)]^0|\Phi\textrm{为任一含自由变元}x\textrm{的一阶公式}\}\).
这里 \(B^0\)表示 B 的全称封闭式。又令 $$MC(A)=\Omega(A)\cup\{A\},$$
\(MC(A)\) 称为 A 的最小完备集。
如果 \(MC(A)\vdash_{FSFC}B\), 则称一阶公式 B 由一阶公式 A 限定论可证，记为 \(A\sdash_{mc}B\).
限定一阶语言仅含一个一元谓词 P(x), 有 \(\exists x P(x)\sdash_{mc}\forall x P(x)\).
限定论可证的非单调性：当限定被取消或改变时。
限定理论的语义
设 \(\Gamma\) 为一阶命题集，称结构 \(\mathfrak {A}=\lt U, I\gt\) 为 \(\Gamma\) 的
最小模型，
如果
-
对每个 \(A\in\Gamma, \models_{\mathfrak{A}} A\).
-
对 \(\mathscr{U}\) 的任一子结构 \(\mathfrak{A}'=\lt U', I'\gt(U'\subset U, I'=I\mid_{U'}, I\mid_{U'}\) 表示将解释 I 限于 \(U'\), 例如对一元谓词 P, \(I\mid_{U'}(P)=I(P)\cap U')\)
存在 \(A\in\Gamma\), 使 \(\not\models_{\mathfrak{A}'} A\).
称一阶命题 B 为一阶命题集 \(\Gamma\) 的最小逻辑结果, 记为 \(\Gamma\models_{mc} B\),
如果 B 在所有 \(\Gamma\) 的最小模型中均真。
见书上例子。
\(\Gamma_1=\emptyset\), 其最小模型为所有个体域为幺元集的结构，
有 $$\Gamma_1\models_{mc}\forall x\forall y(x=y)$$.
\(\Gamma_2=\{\exists x\exists y(x\neq y)\}\), 其最小模型为所有个体域含有两个元素的结构，
有 $$\Gamma_2\not\models_{mc}\forall x\forall y(x=y)$$.
上面例子说明 \(\models_{mc}\) 不是单调的。
限定可证性的合理性和完备性
对任何一阶命题 A, B, 如果 \(A\sdash_{mc} B\), 则 \(A\models_{mc} B\).
设 \(\mathfrak{A}=\lt U, I\gt\) 为 A 的最小模型，C 为 \(\Omega(A)\) 中的任一公式。
先证 \(\models_{\mathfrak{A}} C\).
只需证 \(\models_{\mathfrak{A}}[A^{\Phi}\to\forall x\Phi(x)]^0\).
将论域限定到满足 \(\Phi\) 的个体集上即可。
再证 \(A\models_{mc} B\).
将 \(\sdash_{mc}\) 转化到 FSFC上即可。
限定可证性不具有完备性。
考虑例 11.18.
性质限定
“船可以渡河”：
设 \(A(\vec P)\) 为一二阶公式， \(\vec P\) 为一组谓词变元 \(P_0,\dots,P_n\) 的缩写。
又设 \(E(\vec P, \vec x)\) 是含自由谓词变元 \(P_0,\dots,P_n\) 和个体变元
\(x_1,\dots,x_m\) 的二阶公式。称下列二阶公式为 \(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) 的性质限定为：
\(\forall P'(A(P')\land\forall x(E(P',x)\to E(P,x))\to\forall x(E(P',x)\leftrightarrow E(P,x)))\)
如果一个船的性质是“能渡河”的子属性，则这个性质就是“能渡河”。
性质限定(续)
\(A(\vec P), \vec P\) 的意义同定义 11.15,称下列二阶公式为 A 中
谓词变元 \(P_0\) 具有 \(P_1,\cdots,P_n\) 的限定，
记为 \(Circum(A;P_0,P_1,\cdots,P_n)\)：
\(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) 表示如下事实：
$$\forall x(Dx\leftrightarrow\lnot Lx)\land La\land Db\land Rc\land(a\neq b\land a\neq c\land b\neq c)$$
其中 Dx 表示 x 死了， Lx 表示 x 活着，Rx 表示 x 是兔子，
想要限定“全部死了的客体就是已知死了的客体(即 b)”。
只用之前的限定方法限定 D，由于无法推出 \(\lnot 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)$$
令 \(P_0(x)\) 为 \(x=b\), \(P_1(x)\) 为 \(x\neq b\)，即得
$$\forall x(x=b\leftrightarrow Dx)$$
即得我们想要的结果。
性质限定的可满足性
如果 \(A(\vec P)\) 的限定是可满足的，那么 \(A(\vec P)\) 也是可满足的，但反之不然。
见书上例 11.21
如果 \(A(\vec P)\) 为一可满足的
全称命题
前束范式中不含存在量词
，那么 \(Circum(A(\vec P), \vec P)\) 也是可满足的。
限定理论的应用前景
Frame problem: 在动作后状态的改变只局限在动作影响到的部分上。
Thank you!