Skip to main content
SpringerLink
Log in
Book cover

International Conference on Knowledge Based Computer Systems

KBCS 1989: Knowledge Based Computer Systems pp 296–305Cite as

On the completeness of narrowing for E-unification

  • Logic Programming
  • Conference paper
  • First Online:

  • 1956 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 444))

Abstract

The narrowing mechanism has been a major tool in designing complete E-unification procedures for classes of equational theories in the last few years. Meanwhile, it has also been noticed that it is sometimes difficult to build complete procedures using only the narrowing mechanism. This paper analyzes several examples encountered by the authors in the course of research, which show that in certain situations narrowing fails to yield a complete E-unification procedure. Furthermore, we augment the narrowing mechanism with a restricted form of the paramodulation rule. This yields a complete E-unification procedure for all the equational theories that can be described by a confluent term rewriting system. We then present a new procedure in which paramodulation is eliminated by using a set of preconstructed terms, called cover set, which is a substantially reduced set of terms of certain complexity. This provides a degree of completeness, called relative completeness, which is measured by complexity of terms.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Brand, D., Proving theorems by the modification method. SIAM J. of Computing, Vol. 4, pp. 412–430, 1975.

    Google Scholar 

  2. Dershowitz, H., Computing with rewrite rules. Information and Control, May/June, 65, 2/3, 1985.

    Google Scholar 

  3. Fay, M.J., First-order unification in an equational theory. in 4th Workshop on Automated Deduction, pp. 161–167, 1979.

    Google Scholar 

  4. Fribourg, L., Oriented equational clauses as a programming language. J. of Logic Programming, Vol 2, pp. 165–177, 1984.

    Google Scholar 

  5. Fribourg, L., A superposition oriented theorem prover. Theoretical Computer Science, Vol. 1, 1985.

    Google Scholar 

  6. Fribourg, L., SLOG: A logic programming language interpreter based on clausal superposition and rewriting. Proc. Symposium on Logic Programming, pp. 172–184, Boston, Mass., July, 1985.

    Google Scholar 

  7. Henschen, L., Private communication, 1985.

    Google Scholar 

  8. Hsiang J. and M. Rusinowitch, A new method for establishing refutational completeness in theorem proving. Proc. of 8th Conference on Automated Deduction, LNCS 230, pp. 141–152, 1986.

    Google Scholar 

  9. Hullot, J.M., Canonical forms and unification. Proc. 5th Conference on Automated Deduction, pp. 318–334, 1980.

    Google Scholar 

  10. Knuth, D. and P. Bendix, Simple word problems in universal algebras. Computational problems in abstract algebra, ed. J. Leech, pp. 163–279, Pergamon Press, 1970.

    Google Scholar 

  11. Loveland, D.W., Automated theorem proving: a logical basis, Norther-Holland, New York, 1978.

    Google Scholar 

  12. O'Donnell, M., Computing in systems described by equations. LNCS 58, Springer-Verlag, New York, 1977.

    Google Scholar 

  13. Peterson, G.E., A technique for establishing completeness results in theorem proving with equality. SIAM J. of Computing, Vol. 12, No. 1, pp.82–100, 1983.

    Google Scholar 

  14. Plotkin, G., Building-in equational theories. Machine Intelligence 7, pp. 73–90, Edinburgh University Press, 1972.

    Google Scholar 

  15. Reddy, U., Narrowing as the operational semantics of functional languages. Proc. Symposium on Logic Programming, pp. 138–151, Boston, Mass., July, 1985.

    Google Scholar 

  16. Robinson, G. and L. Wos, Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence 4, B. Meltzer and D. Michie, eds., Edinburgh University Press, Edinburgh, 1969, pp. 135–150.

    Google Scholar 

  17. Siekmann, J., Universal unification, Proc. 7th International Conference on Automated Deduction, pp. 1–42, Napa, Califomia, May, 1984.

    Google Scholar 

  18. You, J.-H. and P.A. Subrahmanyam, A class of confluent term rewriting systems and unification. J. Automated Reasoning Vol. 2, 391–418, 1986.

    Google Scholar 

  19. You, J.-H., Unification Modulo an Equality Theory for Equational Logic Programming. To appear in J. Computer and System Sciences.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta, Canada

    Jia-Huai You

  2. AT&T Bell Laboratories, 07733, Holmdel, NJ

    P. A. Subrahmanyam

Authors
  1. Jia-Huai You
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. A. Subrahmanyam
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Ramani R. Chandrasekar K. S. R. Anjaneyulu

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

You, JH., Subrahmanyam, P.A. (1990). On the completeness of narrowing for E-unification. In: Ramani, S., Chandrasekar, R., Anjaneyulu, K.S.R. (eds) Knowledge Based Computer Systems. KBCS 1989. Lecture Notes in Computer Science, vol 444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018388

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52850-0

  • Online ISBN: 978-3-540-47168-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation