• Articles • Previous Articles     Next Articles

A Goal-Type Driven Method of Solving Horn Logic with Equality

Hu Yunfa;   

  1. Changsha Institute of Technology Hunan;
  • Online:1990-05-10 Published:1990-05-10

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…

[1] J.A.Goguen and J.Mesequer. Equality, Types, Modules and Generic for Logic Programming. Proc. 2nd Int .Logic Programming Conf., Uppsala,1984,115-125.

[2] A.Martelli, C.Moiso, G.F.Rossi, An Algorithm for Unification Equational Theories, Proc.Symp. Logic Programming, Utah, 1986, PP.180-196.

[3] V.J.Digricoli, M.C.Harrison, Equality-based binary resolution, ACM. 33:2 (1986). 253-289.

[4] P.A.Subrahmanyam, H.J.You, Conceptual Basis and Evaluation Strategies for Integrating Function and Logic Programming, Proc.IEEE Int .Symp .Logic Programming. Atlantic City, N.J., February 1984,144-153.

[5] A.Josephson and N.Dershowitz, An Implementation of Narrowing: The RITE Way. Proc. Symp. Logic Programming, Utah, 1986, 187-196.
No related articles found!
Full text



No Suggested Reading articles found!

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved