A Goal-Type Driven Method of Solving Horn Logic with Equality
胡运发 · 1990
A new method of solving Horn logic with equality,the goal-type driven method,is presented,which considers explicitly the unification operator as a gloal and merged it into the resolution process,The metho 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 language by a uniform framework.It can also deal with infinite data structures.