联合正规形式的子句包含正面和负面文字，可以在表单中表示
（¬阿1 ∨…∨¬上午∨乙1 ∨…∨ BN）
变量A 1 ，…，Am和B 1 ，…，Bn。该子句可以通过两个简单的步骤转换为等效形式
阿1 ∧…∧上午⇒乙1 ∨…∨ BN。
这个含义包含前提，变量与结论的结合，变量的分离。例如，“ 如果天气好，地面上有雪，我会去滑雪，或者我会工作。”这是这种形式的主张。该消息的接收者肯定知道发送者不会游泳。一个更明确的说法是“ 如果天气好，地面上有雪，我会去滑雪。” 接收器现在明确知道。因此，我们称条款最多只有一个正面的字面明确条款。这些条款的优点是它们只允许一个结论，因此解释起来明显简单。许多关系可以用这种类型的条款来描述。因此我们定义
定义2.10 条款最多只有一个正面的文字形式
（¬阿1 ∨…∨¬上午∨ B）或（¬阿1 ∨…∨¬上午）或乙
或（等效地）
阿1 ∧…∧上午⇒乙或阿1 ∧…∧上午⇒ ˚F 或 B.
被命名为Horn条款（在他们的发明者之后）。具有单个正文字的子句是事实。在具有否定和一个正面文字的条款中，正面文字称为头部。
为了更好地理解Horn子句的表示，读者可以从我们当前使用的等价的定义中得出它们（第 30 页的实践 2.12 ）。
∧
Horn条款不仅在日常生活中更容易处理，而且在正式推理中也更容易处理，我们可以在下面的例子中看到。让知识库由以下子句组成（“绑定子句在此处和后面的文本中省略）：
（不错_天气）1（降雪）2（降雪⇒雪）3
（不错_天气∧雪⇒滑雪）4
如果我们现在想知道滑雪是否成立，这很容易得出。稍微概括的modus ponens在这里作为推理规则就足够了：
阿1 ∧…∧上午，A 1 ∧…∧上午⇒乙。乙
的“证明滑雪 ”具有以下形式（MP （I 1 ，…，IK）表示的作案的应用前件的第我 1至IK：
MP（2，3）： （雪）5
MP（1，5，4）：（滑雪）6。
通过modus ponens，我们获得了一个由命题逻辑Horn子句组成的公式的完整计算。然而，在知识库较大的情况下，如果以错误的条款开头，则模式推导可以导出许多不必要的公式。因此，在许多情况下，最好使用以查询开头并向后工作的微积分，直到达到事实为止。与前向链接系统相比，这种系统被指定为反向链接，前向链接系统以事实开始并最终导出查询，如上例中的模式推理。
对于Horn子句的反向链接，使用 SLD解析。SLD代表“选择规则驱动线性分辨率的明确条款”。在上面的例子中，由否定的查询（滑雪⇒f）增加
（不错_天气）1（降雪）2（降雪⇒雪）3
（不错_天气∧雪⇒滑雪）4
（滑雪⇒f）5
我们执行SLD解决方案，从本节后面的解决步骤开始
RES（5，4）：（不错_天气∧雪⇒ F）6
RES（6，1）：（雪⇒ F）7个RES（7，3）：（降雪⇒ F）8个RE（8，2）：（）
并导致与空条款的矛盾。在这里我们可以很容易地看到“ 线性分辨率 ”，这意味着总是在当前派生的子句上进行进一步处理。这导致搜索空间大大减少。此外，当前子句的文字总是按固定顺序处理（例如，从右到左）（“ 选择规则驱动 ”）。调用当前子句的文字
subgoal 。否定查询的文字是目标。一步的推理规则读取
阿1 ∧…∧上午⇒乙1，B 1 ∧乙2 ∧…∧ BN ⇒ ˚F 。
阿1个∧…∧上午∧乙2 ∧…∧ BN ⇒ ˚F
∧・・・∧
在应用推理规则之前，必须证明B 1 ，B 2 ，…，Bn-当前的子目标。涂布后，乙 1由新次级目标取代甲 1 ∧…∧ 上午。为了表明B 1是真的，我们现在必须证明A 1 Am是真的。这个过程一直持续到当前条款的子目标列表（所谓的目标）
堆栈）是空的。有了这个，就发现了一个矛盾。如果对于一个子目标¬毕，有一个与互补字面没有条款毕其条款头，证明终止并没有矛盾都可以找到。因此该查询是不可证实的。
SLD解析在实践中起着重要作用，因为逻辑编程语言PROLOG中的程序由谓词逻辑Horn子句组成，并且它们的处理是通过SLD解析来实现的（参见第 30 页的练习 2.13 ，或第5章）。
意见反馈