Skip to main content
SpringerLink
Log in

A goal-type driven method of solving Horn logic with equality

  • Regular Papers
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

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 laguage and logic language by a uniform framework. It can also deal with infinite data structures.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  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.

    Article  MathSciNet  Google Scholar 

  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.

Download references

Author information

Authors and Affiliations

  1. Changsha Institute of Technology, Human

    Hu Yunfa

Authors
  1. Hu Yunfa
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hu, Y. A goal-type driven method of solving Horn logic with equality. J. of Comput. Sci. & Technol. 5, 250–258 (1990). https://doi.org/10.1007/BF02945313

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02945313

Keywords

Search

Navigation