论文部分内容阅读
A new method of solving Horn logic with equality,the goal-type driven method,is presented,which considers explicitly the unification operator as a goal and merged it into the resolution process.The method has the following advantages.The resolution and the unification have been integrated in auniform way.The architectures of the inference engines based on Horn logic with equality are simplified.Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification atthe same time.The method can be used to integrate the styles of functional language and logic lan-guage by a uniform framework.It can also deal with infinite data structures.
A new method of solving Horn logic with equality, the goal-type driven method, is presented, which considers explicitly the unification operator as a goal and merged it into the resolution process. The method has the following advantages. The resolution and the unification have been integrated in a uniform way. The architectures of the inference engines based on Horn logic with equality of simplified. Any techniques of exploiting AND / OR parallelism to solve goals can also be applied to unification atthe same time. The method can be used to integrate the styles of functional language and logic lan-guage by a uniform framework. It can also deal with infinite data structures.