联合正规形式的子句包含正面和负面文字,可以在表单中表示
(¬阿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章)。
意见反馈