在AI中，我们感兴趣的是获取现有知识，并从中获取新知识或回答问题。在命题逻辑中，这意味着显示知识库KB，即（可能是广泛的）命题逻辑公式 – 公式Q 1。因此，我们首先定义术语“蕴涵”。
1这里Q代表查询。
定义2.6 公式 KB需要一个式 Q （或 Q如下从 KB ）如果每一个模型 KB 也是一个模型 Q 。我们写 KB | Q 。
换句话说，在KB为真的每个解释中，Q也是如此。更简洁地说，只要KB为真，Q也是如此。因为，对于所涉及的概念，引入了变量的解释，我们正在处理一个语义概念。
∨¬
|
∅|
每个无效的公式都选择将所有解释集的子集作为其模型。例如，诸如AA之类的重言式并不限制令人满意的解释的数量，因为它们的命题是空的。因此，空公式在所有解释中都是正确的。对于每一个同义反复牛逼那么牛逼。直观地说，这意味着重言式始终是真实的，不受公式对解释的限制。对于短期我们写牛逼。现在我们展示了蕴涵的语义概念和句法蕴涵之间的重要联系。
定理2.2 （Deduktionstheorem）
A | B当且仅当| 一个⇒ B.
证明观察真相表的含义：
ABA ⇒乙
TTT
|
Ť |
F |
F |
|
F |
Ť |
Ť |
|
F |
F |
Ť |
⇒⇒
→→|
⇒
除了解释A t，B f之外，任意含义AB显然都是正确的。假设AB成立。这意味着对于使A为真的每一种解释，B也是如此。在这种情况下，真值表的关键第二行甚至不适用。因此AB是真的，这意味着AB是重言式。因此，该陈述的一个方向已经显示出来。
现在假设一个⇒乙持有。因此，真值表的关键第二行也被锁定。然后， A的每个模型也是 B 的模型。然后 A | B 持有。
⇒
如果我们希望证明KB需要Q，我们也可以通过真值表方法证明KB Q是重言式。因此，我们有第一个命题逻辑证明系统，它很容易实现自动化。该方法的缺点是在最坏的情况下计算时间非常长。具体而言，在与最坏的情况下Ñ命题变量，对于所有2个Ñ解释变量的式KB ⇒ Q必须被评估。因此，计算时间呈指数增长
与变量的数量。因此，至少在最坏的情况下，该过程对于大的可变计数是不可用的。
如果公式 KB需要一式 Q，然后通过扣除定理 KB ⇒ Q是一种赘述。因此，否定¬（ KB⇒Q）是不可满足的。我们有
¬ （KB ⇒ Q） ≡¬ （ ¬ KB ∨ Q） ≡ KB ∧¬ Q.
∧¬
因此KB Q也是可以满足的。我们将演绎定理作为一个定理，形成了这个简单而重要的结果。
定理2.3 （矛盾证明） KB | Q当且仅当KB∧¬Q为
不满意。
∧¬⇔
¬
为了表明查询Q来自知识库KB，我们还可以将否定查询Q添加到知识库并导出矛盾。因为等价的AA˚F 从定理2.1 页18，我们知道，一个矛盾是不可满足的。因此，Q已被证明。该程序经常用于数学，也用于各种自动证明计算，例如分辨率计算和PROLOG程序的处理。
|
避免其与真值表方法来测试所有的解释的一种方法是公式的句法操纵KB和Q通过应用的推理规则，大大简化了他们的目标，这样最终我们可以立即看到KB Q。我们称这个过程语法推导和写入KB Q。这种句法证明系统称为计算。为了确保微积分不会产生误差，我们定义了微积分的两个基本属性。
定义2.7如果每个派生命题都遵循语义，则称微积分称为声音。也就是说，如果持有的公式KB和Q是
如果 KB Q 则 KB | Q.
如果可以导出所有语义后果，则称微积分为完全。也就是说，对于公式KB和Q，它包含以下内容：
如果 KB | Q 然后 KB Q.
微积分的健全性确保所有派生公式实际上是知识库的语义结果。微积分不会产生任何“错误后果”。另一方面，微积分的完整性确保了微积分不会忽略任何东西。如果要证明的公式来自知识库，则完整的微积分总能找到证明。如果微积分是合理的
KB Q.
句法层面
（公式）
Mod （KB）|
Mod （Q）
语义层面
（口译）
蕴涵
求导
解释
解释
图2.1句法推导和语义蕴涵。Mod （X）表示公式X的模型集
然后完成，然后句法推导和语义蕴涵是两个等价的关系（见图 2.1 ）。
为了使自动校样系统尽可能简单，通常使这些系统以连接法线形式运行。
定义2.8当且仅当它由连词组成时，公式为联合范式（CNF）
ķ 1 ∧ ķ 2 ∧…∧公里
条款。一个条款Ki由一个分离组成
（李1 ∨栗2 ∨…∨林我）
文字。最后，文字是变量（正文字）或否定变量（负文字）。
∨∨∧∧∧∨¬
公式（ABC）（AB）（BC）是合并的正常形式。联合正规形式不对公式集设置限制，因为：
定理2.4 每个命题逻辑公式都可以转换为等价的连接范式。
∨ ⇒∧
例2.1 我们通过使用第18 页的定理2.1中的等价来将 ABCD 置于合取范式：
甲∨乙⇒ Ç ∧ d
≡¬（A∨B）∨（C∧D）（暗示）
≡（¬甲∧¬ B）∨（C ∧ d）（德摩根）
≡（¬甲∨（C ∧ d））∧（¬乙∨（C ∧ d））（分配律）
≡（（¬甲∨ C）∧（¬甲∨ d））∧（（¬乙∨ C）∧（¬乙∨ d））（分配律）
≡（¬甲∨ C）∧（¬甲∨ d）∧（¬乙∨ C）∧（¬乙∨ d）（结合律）
⇒
我们现在只缺少命题逻辑公式的句法证明的微积分。我们先从假言推理，推理的一个简单的，直观的规则，其中，从有效性一和AB，允许的推导乙。我们正式写这个
A，A ⇒乙。乙
这种表示法意味着我们可以从线上方的逗号分隔公式得到线下面的公式。Modus ponens作为一个规则，虽然声音，但并不完整。如果我们添加其他规则，我们可以创建一个完整的计算器，但是，我们不希望在此考虑。相反，我们将调查解决规则
甲∨ B，¬乙∨ Ç 甲∨ Ç
（2.1）
作为备选。derived子句称为resolvent。通过简单的转换，我们得到了等价的形式
甲∨ B，B ⇒ Ç 。
一个∨ Ç
如果我们将 A 设置为 f ，我们会看到解析规则是对模态推理的推广。如果 C 缺失或 A 和 C 缺失，则解决规则同样可用。在后者的情况下，空的子句可以从矛盾导出乙∧¬乙（练习2.7 页上的30 ）。
命题逻辑：解析度
我们现在通过允许具有任意数量文字的子句来再次概括解析规则。使用文字A 1 ，…，Am，B，C 1 ，…，Cn，一般分辨率规则读取
（A 1个∨…∨上午∨ B），（¬乙∨ Ç 1 ∨…∨ Cn）的。（2.2）
（A 1 ∨…∨上午∨ Ç 1 ∨…∨ Cn）的
1.
第23号决议
¬
我们称文字B和B互补。解析规则从两个子句中删除一对互补的文字，并将其余的文字组合成一个新的子句。
¬
∧¬
为了证明从知识库KB，查询Q 如下，我们通过矛盾进行证明。按照第20 页的定理2.3 ，我们必须证明可以从KB Q中得出矛盾。在联合正规形式的公式中，矛盾以两个条款（A）和（A）的形式出现，这导致空条款作为其解决方案。以下定理确保我们这个过程真正按预期工作。
∨∧¬∨¬
∧
∨
为了完成微积分，我们需要一个小的补充，如下面的例子所示。让公式（AA）作为我们的知识库。为了通过分辨率规则显示我们可以从中得出（AA），我们必须证明空子句可以从（AA）（AA）导出。仅凭分辨率规则，这是不可能的。通过分解，允许从子句中删除文本副本，可以消除这个问题。在示例中，双重应用程序
因子分解导致（A）∧（¬A），以及空子句的解决步骤。
定理2.5 以连接法线形式证明公式不可满足性的分辨率计算是完整的。
因为从解决方案微积分的工作中得出一个矛盾
KB ∧¬ Q ，这是非常重要的知识基础 KB 是一致的：
定义2.9 公式 KB 被称为一致，如果它是不可能从中得到一个矛盾，即，形式的式 φ ∧¬ φ 。
否则，可以从KB 派生任何内容（参见第 30 页的练习 2.8 ）。这不仅适用于分辨率，也适用于许多其他结石。
在自动演绎的结算中，分辨率起着特殊的作用。因此，我们希望与它更紧密地合作。与其他结石相比，分辨率只有两个推理规则，它与联合正规形式的公式一起使用。这使其实现更简单。与许多计算相比，另一个优点在于减少了在证明的每个步骤中应用推理规则的可能性，从而减少了搜索空间并缩短了计算时间。
作为一个例子，我们从一个简单的逻辑谜题开始，它允许显示分辨率证明的重要步骤。
例2.2 题为一个迷人的英国家庭的逻辑谜题7，来自德国的书[Ber89]读（翻译成英文）：
尽管学习了七年英语并取得了巨大成功，但我必须承认，当我听到英语人士说英语时，我完全感到困惑。最近，由于高贵的感情，我找到了三个搭便车的人，一个父亲，一个母亲和一个女儿，我很快意识到他们是英语，只会说英语。在随后的每一句话中，我都在两种可能的解释之间进行了研究。他们告诉我以下（第二个可能的含义在括号中）：父亲：“我们要去西班牙（我们来自纽卡斯尔）。”母亲：“我们不去西班牙，来自纽卡斯尔（我们停在巴黎，不去西班牙）。“女儿：”我们不是来自纽卡斯尔（我们在巴黎停留）。“这个迷人的英国家庭怎么样？
为了解决这类问题，我们分三步进行：形式化，转换为正常形式和证明。在许多情况下，形式化是迄今为止最困难的一步，因为它容易出错或忘记细节。（因此实际练习非常重要。参见练习 2.9 – 2.11 。）
这里我们使用变量S表示“ 我们要去西班牙 ”，N表示“ 我们来自纽卡斯尔 ”，P表示“ 我们在巴黎停留 ”，并获得父亲，母亲和女儿三个命题的正式化
（S ∨ N）∧[ （¬小号∧ N）∨（P ∧¬ S）]∧（¬ Ñ ∨ P）。
¬
分解出小号中间子式中带来的公式为CNF在一个步骤中。使用下标索引对子句进行编号
KB ≡（S ∨ N）1 ∧（¬ S）2 ∧（P ∨ N）3 ∧（¬ Ñ ∨ P）4。
现在我们开始分辨率证明，起初仍然没有查询Q。“Res （m，n）：from k
” 形式的表达式意味着该子句是通过条款m的解析获得的，其中条款为n，并且编号为k。
RES（1，2）：（N）5
RES（3，4）：（P）6
RES（1，4）：（S ∨ P）7
¬
我们可以得出子句P也从RES （ 4 ， 5 ）或RES （ 2 ， 7 ）。每一个进一步的解决步骤都将导致已经可用的条款的推导。因为它不允许推导空子句，因此已经表明知识库是不矛盾的。到目前为止，我们已经得出ñ和P。为了表明S成立，我们将子句（S） 8作为否定查询添加到子句集中。随着决议步骤
RES（2，8）： （）9
∧∧∧
证明完整。因此SNP成立。“迷人的英国家庭”显然来自纽卡斯尔，在巴黎停留，但不会去西班牙。
实施例2.3 逻辑拼图数28从[Ber89]，题为跳高，读取
三个女孩为他们的体育期末考试练习跳高。酒吧设置为1.20米。“我打赌”，第二个女孩说到第二个，“如果，只有当你不这样做时，我会把它翻过来”。如果第二个女孩对第三个女孩说同样的话，那个人又对第一个说同样的话，这三个人都有可能赢得他们的赌注吗？
我们通过决议证明，并非所有三个人都能赢得他们的赌注。
形式化：
第一个女孩的跳跃成功： A ，第一个女孩的赌注：（A⇔¬B），第二个女孩的跳跃成功： B ，第二个女孩的赌注：（B⇔¬C），第三个女孩的跳跃成功： C 。第三个女孩的赌注：（C⇔¬A）。
声明：三人不可能都赢得他们的赌注：
Q ≡¬（（A ⇔¬ B）∧（B ⇔¬ C）∧（C ⇔¬ A））
¬
现在必须通过决议表明Q不可满足。
转型为CNF ：第一个女孩的赌注：
（A ⇔¬ B）≡（A ⇒¬ B）∧（¬乙⇒ A）≡（¬甲∨¬ B）∧（A ∨ B）
其他两个女孩的赌注经历了类似的转变，我们获得了否定的主张
¬ Q ≡ （ ¬ 甲 ∨¬ B）1 ∧ （A ∨ B）2 ∧ （ ¬ 乙 ∨¬ C）3 ∧ （B ∨ C）4 ∧ （ ¬ ç ∨¬ A）5
∧（C∨A）6。
从那里我们使用解决方案派生空子句：
RES（1，6）： （C ∨¬ B）7
RES（ 4， 7）： （C） 8
RES（2，5）： （B ∨¬ C）9
RES（3，9）： （¬ C）10
RES（8，10）： （）
因此，该声明已得到证实。
