基于逻辑的模型
基础
命题逻辑语法 记 、为公式，、、、、为连接词，我们可以写出以下逻辑表达式：
| | | |
| | |  |
| | |  |
| | |  |
| | |  |
| | |  |
| | |  |
备注： 公式可以通过这些连接词递归地构建。
模型 模型 表示对命题符号的二元权重分配。
示例： 真值集合 是命题符号 、和 的一种可能模型。
解释函数 解释函数 输出模型 是否满足公式 ：
模型集合 表示满足公式 的模型 的集合。数学上，我们定义如下：
知识库
定义 知识库 是迄今为止考虑的所有公式的合取。知识库的模型集合是满足每个公式的模型集合的交集。换句话说：
概率解释 查询 被评估为 的概率可以看作知识库 中满足 的模型 的比例，即：
可满足性 如果至少有一个模型 满足知识库 的所有约束，则称知识库 是可满足的。换句话说：
备注： 表示与知识库所有约束兼容的模型集合。
公式与知识库之间的关系 我们定义知识库 和新公式 之间的以下性质：
| | | |
| | | |
| | | |
| | | |
模型检查 模型检查算法以知识库 为输入，输出它是否可满足。
备注： 流行的模型检查算法包括 DPLL 和 WalkSat。
推理规则 前提 和结论 的推理规则写作：
前向推理算法 从一组推理规则 出发，该算法遍历所有可能的 ，如果存在匹配的规则，则将 添加到知识库 。这个过程重复进行，直到无法再向 添加更多内容。
推导 如果 已经在 中，或者在前向推理算法期间使用规则集 被添加，我们说 用规则 推导出 （写作 ）。
推理规则的性质 一组推理规则 可以具有以下性质：
| | |
| | |
| | |
命题逻辑
在本节中，我们将介绍使用逻辑公式和推理规则的基于逻辑的模型。这里的想法是平衡表达能力和计算效率。
Horn 子句 记 和 为命题符号，Horn 子句具有以下形式：
备注： 当 时，称为“目标子句”，否则我们将其表示为“确定子句”。
肯定前件 对于命题符号 和 ，肯定前件规则写作：
备注： 应用此规则需要线性时间，因为每次应用生成一个包含单个命题符号的子句。
完备性 如果我们假设 仅包含 Horn 子句，且 是一个被蕴含的命题符号，则肯定前件关于 Horn 子句是完备的。应用肯定前件将推导出 。
合取范式 合取范式（CNF）公式是子句的合取，其中每个子句是原子公式的析取。
备注： 换句话说，CNF 是 的 。
等价表示 命题逻辑中的每个公式都可以写成等价的 CNF 公式。下表呈现了一般的转换性质：
| | |
| | |
| | |
| | |
| | |
| | |
| | |
归结规则 对于命题符号 和 以及 ，归结规则写作：
备注： 应用此规则可能需要指数时间，因为每次应用生成一个具有命题符号子集的子句。
基于归结的推理 基于归结的推理算法遵循以下步骤：
•
步骤 1： 将所有公式转换为 CNF
•
步骤 2： 重复应用归结规则
•
步骤 3： 当且仅当推导出 时返回不可满足
一阶逻辑
这里的想法是使用变量来产生更紧凑的知识表示。
模型 一阶逻辑中的模型 映射：
•
常量符号到对象
•
谓词符号到对象元组
Horn 子句 记 为变量，为原子公式，Horn 子句的一阶逻辑版本具有以下形式：
替换 替换 将变量映射到项，表示替换 在 上的结果。
合一 合一取两个公式 和 ，返回使它们相等的最一般替换 ：
注意： 如果不存在这样的
θ
，
Unify[f,g]
返回
Fail
。
肯定前件 记
x1,...,xn
为变量，
a1,...,ak
和
a1′,...,ak′
为原子公式，并调用
θ=Unify(a1′∧...∧ak′,a1∧...∧ak)
，肯定前件的一阶逻辑版本可以写作：
Subst[θ,b]a1′,...,ak′∀x1,...,∀xn(a1∧...∧ak)→b
完备性 肯定前件对于仅含 Horn 子句的一阶逻辑是完备的。
归结规则 记
f1,...,fn
、
g1,...,gm
、
p
、
q
为公式，并调用
θ=Unify(p,q)
，归结规则的一阶逻辑版本可以写作：
Subst[θ,f1∨...∨fn∨g1∨...∨gm]f1∨...∨fn∨p,¬q∨g1∨...∨gm
半可判定性 一阶逻辑，即使仅限制为 Horn 子句，也是半可判定的。
•
如果
KB⊨f
，对完备推理规则的前向推理将在有限时间内证明
f
•
如果 ，没有算法可以在有限时间内证明这一点