2023-12-04 12:00:00-0400
模型的域 (domain) 是一个非空集合，包含模型的对象。
模型中的对象间可能有关系 (relation)，关系是相关对象的元组集。
一阶逻辑中的模型需要全函数 (total function)，对所有输入的对象或元组都有输出。
一阶逻辑的基本语法元素包括:
每个模型必须提供所需的信息来确定任意给定语句为真还是为假。因此，除了它的对象、关系和函数，每个模型还要包含一套确切指明常量、谓词和函数符号指代的是哪个对象、关系和函数的解释 (interpretation)。
一阶逻辑中的模型包含一个对象集和一种解释，这种解释将常量符号映射到对象、将函数符号映射到关于这些对象的函数，将谓词符号映射到关系。与命题逻辑一样，蕴含、有效性等都是用所有可能模型来定义的3。
项是指代对象的逻辑表达式，可以是常量或函数的值 (函数应用于对象而产生的对象)。
将指代对象的项与指代关系的谓词符号结合起来，就可以得到原子语句4。
如果谓词符号所指代的关系在参数所指代的对象之间成立，则在给定模型中原子句为真。
复合语句是由原子语句和逻辑连接词 (logical connective) 构成的语句。比如，\(P(x,y) \land Q(x)\)。
量词是用来指定变量的范围的；一阶逻辑中有两种量词：全称量词 (universal quantifier) \(\forall\) 和存在量词 (existential quantifier) \(\exists\)，它们的关系为:
\[ \begin{aligned} \lnot \forall x P(x) &\equiv \exists x \lnot P(x) & \lnot (P \lor Q) &\equiv \lnot P \land \lnot Q \\ \lnot \exists x P(x) &\equiv \forall x \lnot P(x) & \lnot (P \land Q) &\equiv \lnot P \lor \lnot Q \\ \forall x P(x) &\equiv \lnot \exists x \lnot P(x) & P \land Q &\equiv \lnot (\lnot P \lor \lnot Q) \\ \exists x P(x) &\equiv \lnot \forall x \lnot P(x) & P \lor Q &\equiv \lnot (\lnot P \land \lnot Q) \end{aligned} \]
一般来说，\(\forall\)通常和\(\Rightarrow\)一起使用，\(\exists\)通常和\(\land\)一起使用。
\[ \begin{aligned} \forall x & At(x, Berkeley) \Rightarrow Smart(x)\\ \exists x & At(x, Berkeley) \land Smart(x) \end{aligned} \]
一种错误的表达是\(\forall x At(x, Berkeley) \land Smart(x)\)，他的意思是所有人都在伯克利并且聪明，而不是在伯克利的人都聪明。
等词表示两个项指代的对象相等，它是一种特殊的谓词符号，用 \(=\) 表示；\(x\neq y\) 可以表示为 \(\lnot (x=y)\)。
语句是通过Tell添加到知识库的，与在命题逻辑中完全一样，这种语句被称为断言 (assertion)。
\[ Tell(KB, Person(John)) \]
使用Ask提出的问题被称为查询或目标 (query)。
\[ Ask(KB, Person(John)) \]
返回的结果是一个布尔值，表示查询是否为真，这里返回的结果是真。也可以提出量化的问题:
\[ Ask(KB, \exists x Person(x)) \]
这里返回的结果是真，因为存在一个人。但我们更想知道的是这个人是谁，所以我们可以使用AskVars，它返回一个变量的绑定 (binding) 列表/置换 (substitution)，这里返回的结果是\(\{x/John\}\)。
本节演示了如何使用一阶逻辑来表示数字、集合和列表。
以定义自然数为例，需要谓词\(NatNum\)判断一个对象是否是自然数，常量符合\(0\)和后继函数\(S\)。
\[ NatNum(0) \\ \forall n\; NatNum(n) \Rightarrow NatNum(S(n)) \]
\[ \begin{aligned} &\forall n\; 0\neq S(n) \\ &\forall m,n\; S(m)\neq S(n) \Rightarrow m\neq n \end{aligned} \]
\[ \begin{aligned} &\forall n\; NatNum(n) \Rightarrow Add(0, n) = n \\ &\forall m,n\; NatNum(m) \land NatNum(n) \Rightarrow Add(S(m), n) = S(Add(m, n)) \end{aligned} \]
\[ \lnot \exists x,s\; Add(x, s)=\{\} \]
\[ \forall x,s\; x\in s \Leftrightarrow Add(x, s)=s \]
全程量词实例化 (universal instantiation) 和存在量词实例化 (existential instantiation) 是一阶逻辑中的两种推理规则，通过使用置换 (substitution) 来实现。
通俗来说，全称量词实例化就是用全部合规的指代对象的项替换量词变量。
\[ \frac{\forall x\; \alpha}{SUBST(\{x/t\},\alpha)} \\ \]
\(\alpha\)是一个语句，\(x\)是全称变量，\(t\)是项，\(SUBST(\{x/t\},\alpha)\)表示将\(\alpha\)中的\(x\)替换为\(t\)。
存在量词实例化就是用一个尚未指代对象的常量符号替换量词变量。
\[ \frac{\exists x\; \alpha}{SUBST(\{x/k\},\alpha)} \\ \]
\(\alpha\)是一个语句，\(x\)是存在变量，\(k\)是没有出现过的常量符号，\(SUBST(\{x/k\},\alpha)\)表示将\(\alpha\)中的\(x\)替换为\(k\)。
使用量词实例化可以将一阶知识转化为知识库的知识，此时消去了量词；接下来可以用命题符号替换原子语句，此时消去了谓词符号和函数符号；最后可以用命题逻辑的推理规则来推理。
一阶逻辑的蕴含问题是半可判定的，也就是，存在能判定所有蕴含的语句的算法，却不存在能够判定所有不蕴含的语句的算法
一般化肯定前件 (generalized Modus Ponens): 对于原子语句\(p_i\), \(p_i^{\prime}\)和\(q\)，存在置换使得对所有\(i\)有\(SUBST(\theta, p_i)=SUBST(\theta, p_i^{\prime})\)，则有
\[ \frac{p_1^{\prime},\dots,p_n^{\prime},(p_1\land\dots\land p_n)\Rightarrow q}{SUBST(\theta, q)} \]
这个推理规则有\(n+1\)个前提，其中\(n\)个是原子语句，最后一个是蕴含语句，结论是对后件\(q\)置换的结果。
合一算法的输入是两个语句，输出是一个合一子 (unifier)，它是一个置换，将两个语句中的变量替换为项，使得两个语句相等。
\[ UNIFY(p, q) = \theta \text{ if } SUBST(\theta, p)=SUBST(\theta, q) \]
有时对两个语句进行合一时，为避免变量名称冲突，需要对其中一个语句进行重命名，这个过程称为标准化分离 (standardizing apart)。
每一对可合一的表达式都有一个最一般的合一子 (most general unifier, mgu)
给定要存储的语句，可以对所有可能与之合一的查询构建索引，构成一个包容格 (subsumption lattice)。
graph LR;
id1["P(x,y)"] --> id2["P(John, y)"];
id1 --> id3["P(x, Jane)"];
id2 --> id4["P(John, Jane)"];
id3 --> id4;graph LR;
id1["P(x,y)"] --> id2["P(John, y)"];
id1 --> id3["P(x, John)"];
id1 --> id4["P(x, x)"];
id2 --> id5["P(John, John)"];
id3 --> id5;
id4 --> id5;一阶确定子句是文字的析取式，必须有且仅有一个正文字，要么是原子的，要么是前件为正文字的合取且后件为单个正文字的蕴含语句。
\[ \begin{aligned} & P(x) \land Q(x) \Rightarrow R(x) \\ \text{等价于} \lnot& (P(x) \land Q(x)) \lor R(x) \\ \text{等价于} \lnot& P(x) \lor \lnot Q(x) \lor R(x) \end{aligned} \]
从事实出发，触发所有前提被满足的规则，将结论添加到事实中，重复这个过程直到查询被证明为真或者无法推理出新的结论5。
在前向链接终止时，每个可以用前向链接得出的语句已经显式地被纳入知识库，这种知识库被称为推断过程的不动点。对一阶确定子句使用前向链接得到的不动点和对命题逻辑使用前向链接得到的不动点是类似的，区别在于一阶确定子句的不动点可以包含含有全称量词的语句。
反向链接是一种AND-OR搜索，它从查询开始，尝试找到一个能够证明查询为真的证据，或的部分是对知识库中规则的搜索，而且的部分是对所有前提/合取子句的搜索。
与命题类似，一阶逻辑的合取范式是由合取项构成的析取式，每个合取项都是一个一阶逻辑的析取式，允许包含全称量词。一阶逻辑命题的合取范式可以通过以下步骤得到:
互补的逻辑命题可以通过归结 (resolution) 得到一个新的命题；类似地，如果两个一阶逻辑中的文字能够与另一个文字的否定合一，那么这两个文字就是互补的，它们可以通过归结得到一个新的文字。
\[ \frac{p_1\lor\dots\lor p_n,\; q_1\lor\dots\lor q_m}{SUBST(\theta, p_1\lor\dots\lor p_{i-1}\lor p_{i+1}\lor\dots\lor p_n\lor q_1\lor\dots\lor q_{j-1}\lor q_{j+1}\lor\dots\lor q_m)} \text{ 其中 } UNIFY(p_i, \lnot q_j)=\theta \]
通过合一子\(\theta\)消去互补的文字生成新的归结子句，这个规则叫做二元归结 (binary resolution)。
BFS的将析取子句两两归结，将归结子句添加到子句集中，直到得到空子句，或者无法再进行归结。
纯文字删除策略: 如果对于某个文字\(L\)，在子句集中不存在其互补文字\(\lnot L\)，那么\(L\)就是纯文字；纯文字不影响归结的结果，因此可以从子句集中删除。
重言式删除: 重言式是永真的子句；如果一个子句中包含\(\lnot L\)和\(L\)，那么这个子句就是重言式，可以从子句集中删除6
支持集策略: 每次归结的两个子句中至少有一个是由目标公式的否定所得到的或它们的子节点；支持集策略是完备的；支持集策略限制了宽度而增加了深度
单文字子句策略: 每次归结的两个子句中至少有一个是单文字子句；单文字归结有助于降低归结式的文字数量；单文字子句策略是不完备的
祖先过滤策略7: 满足以下两个条件的任意一个就可以归结