iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/3-540-55602-8_193
Some termination criteria for narrowing and E-narrowing | SpringerLink
Skip to main content
Springer Nature Link
Log in

Some termination criteria for narrowing and E-narrowing

  • Conference paper
  • First Online:
Automated Deduction—CADE-11 (CADE 1992)

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

Included in the following conference series:

Abstract

Given a set of first-order equations T, we describe some restrictions on T which ensure that there are no infinite narrowing derivations using T. The criteria are also applicable when T is used to perform E-narrowing modulo a set of simple linear permutative equations E.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Jacques Chabin and Pierre Réty. Narrowing directed by a graph of terms. Springer-Verlag LNCS 488, Rewriting Techniques and Applications 1991, 112–123.

    Google Scholar 

  2. H. Comon, M. Haberstrau, and J.-P. Jouannaud. Decidable problems in shallow equational theories. Research report, LRI, December 1991.

    Google Scholar 

  3. Nachum Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

    Google Scholar 

  4. Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 1987.

    Google Scholar 

  5. Michael Fay. First-order unification in an equational theory. In Proceedings of the Fourth Workshop on Automated Deduction, pp161–167, Austin, Texas 1979.

    Google Scholar 

  6. G. Huet and B. Lang. Proving and applying program transformations expressed with second-order logic. Acta Informatica 11, 31–55, 1978.

    Google Scholar 

  7. J.-M. Hullot. Canonical forms and unification. Proceedings of the Fifth Conference on Automated Deduction, Les Arcs, France. pp318–334, July 1980.

    Google Scholar 

  8. Dallas Lankford. On proving term rewriting systems are noetherian. Technical Report MTP-3, Dept. of Mathematics, Louisiana Tech University, Ruston, Louisiana, 1979.

    Google Scholar 

  9. P. Rety, C. Kirchner, H. Kirchner, and P. Lescanne. Narrower: a new algorithm for unification and its application to logic programming. In Lecture Notes in Computer Science 202, Springer-Verlag, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa, Sakyo-ku, 606, Kyoto, Japan

    Jim Christian

Authors
  1. Jim Christian
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Christian, J. (1992). Some termination criteria for narrowing and E-narrowing. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_193

Download citation

  • DOI: https://doi.org/10.1007/3-540-55602-8_193

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55602-2

  • Online ISBN: 978-3-540-47252-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation