另一个非常高效的专用推理系统与等价性推理相关。直接将等价性作为公理放到定理证明系统中是很难的。这是因为，对同一个对象而言如果只是使用两个不同的名字，将很难表示出两个不同但等价的公式。但是，有一种有效的算法，能够记录基于等价类的基项之间的等价信息。如果这些技术能够集成到合一程序中，就不需要直接将等价性作为公理写到系统中。相反，扩展的合一算法将用等价程序来检查两个项是否等价并进而合一。
其他几种专用的推理系统可以这样实现：在系统中集成某些专门定义的程序，这些程序用来确定一些特定谓词的真值。这种技术称为附属程序。例如，思考一下时间的推理。虽然可以用时间公理化来驱动时间性的推理，但这样的系统效率很低。有些专门的推理技术能有效地管理时间信息，因此可以作为特殊的谓词集成到综合系统中。为了理解这一点，我们分析命题在一个推理系统中充当的角色。一般有三种不同的操作可应用于命题：
断言为真（即，将其添加到KB中）
查询它是否为真（即，激活定理证明程序来加以验证）
撤销它（即，将其从知识库中删除）
虽然每个操作都是用定理证明系统中的术语来定义的，但这并不表示它是完成这些操作的惟一途径。事实上，可以定义任意过程来执行每一个任务。例如，考虑一个特定的时间推理系统，它维护一个时间关系图，并使用图搜索技术来构建时间关系。假定知识库中有一个谓词“BEFORE”，表示一个时间在另一个之前。当命题（BEFORE t1 t2）加到知识库中时，这个特定的时间推理过程就被激活，并将信息加到时间图中去。在查询同样的命题时（或者是直接由用户提出的查询，或者是一个复杂证明过程的其中一步)，系统就调用该特定的时间推理过程来进行构造。这样，这个专用的时间推理程序就完全集成到定理证明程序中，并且一旦需要时间性信息时就会调用。当然，要完全集成起来，这种专用的推理还要能处理变量并返回与合一等价的结果。例如，定理证明程序需要构造(BEFORE t1 ?x)，那么时间推理程序就要返回一个对?x的约束。除此之外，当需要寻找另一个答案时，还要能处理回溯。
为将专用的推理算法集成到统一的框架中，综合推理系统提供了一种很有吸引力的方法。
责任编辑：admin
上一篇：定义局部篇章上下文和篇章实体
下一篇：程序语义学与问答系统
微信公众号搜索“译员”关注我们，每天为您推送翻译理论和技巧，外语学习及翻译招聘信息。