摘要
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 are simplified. Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification at the 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 are simplified. Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification at the 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.
