【摘要】 本文提出一种处理带等词的Horn逻辑的新方法——目标类型驱动法,它显式地把一致化操作看作目标,并且一致化操作并入归结过程之中。本方法的优点有:(1)把归结和一致化看作多类型目标的求解过程,减化了控制问题,可望提高系统的实现效率;(2)相应的推理机的系统结构,可以得到简化;(3)开发逻辑程序与或并行性的任何技术,同时可应用到一致化过程之中;(4)本方法可用来合成函数程序设计和逻辑程序设计;(5)本方法可用来处理无限数据结构。更多还原

【Abstract】 This paper presents a new method to resolve Horn logic with equality, goal type driven method, in which unification operator is considered as a goal and merged into resolution process.The advantages of the method are as follows:(1) The resolution and the unification are integrated in a uniform way to raise the efficiency of the implementation for Horn logic system. (2) The system architecture of inference engine can be reduced. (3) Any techniques of developing and-or parallel to resolve goals can be applied to unification at the same time. (4) The method can be applied to integrate both the functional language and the logic language. (5) The method can deal with no terminating rewrite rules defining on infinite data structures.更多还原