Skip to main content
SpringerLink
Log in

Proving innermost normalisation automatically

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1232))

Included in the following conference series:

Abstract

We present a technique to prove innermost normalisation of term rewriting systems (TRSs) automatically. In contrast to previous methods, our technique is able to prove innermost normalisation of TRSs that are not terminating.

Our technique can also be used for termination proofs of all TRSs where innermost normalisation implies termination, such as non-overlapping TRSs or locally confluent overlay systems. In this way, termination of many (also non-simply terminating) TRSs can be verified automatically.

This work was partially supported by the Deutsche Forschungsgemeinschaft under grant no. Wa 652/7-1 as part of the focus program “Deduktion”.

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.

References

  1. T. Arts and J. Giesl. Termination of constructor systems. In Proceedings of RTA-96, LNCS 1103, pages 63–T7, 1996.

    Google Scholar 

  2. T. Arts and J. Giesl. Proving innermost normalisation automatically. Tech. Report IBN 96/39, TH Darmstadt, 1996. http://kirmes.inferenzsysteme. informatik.th-darmstadt.de/∼reports/notes/ibn-96-39.ps

    Google Scholar 

  3. T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In Proceedings of CAAP'97, LNCS, 1997.

    Google Scholar 

  4. T. Arts. Termination by absence of infinite chains of dependency pairs. In Proceedings of CAAP'96, LNCS 1059, pages 196–210, 1996.

    Google Scholar 

  5. T. Arts and H. Zantema. Termination of logic programs using semantic unification. In Proceedings of LoPSTr'95, LNCS 1048, pages 219–233, 1995.

    Google Scholar 

  6. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9:137–159, 1987.

    Article  Google Scholar 

  7. F. Bellegarde and P. Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication and Computing, 1:79–96, 1990.

    Google Scholar 

  8. N. Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212–215, 1979.

    Article  Google Scholar 

  9. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 and 2):69–116, 1987.

    Google Scholar 

  10. N. Dershowitz and C. Hoot. Natural termination. Theoretical Computer Science, 142(2):179–207, 1995.

    Article  Google Scholar 

  11. J. Giesl. Generating polynomial orderings for termination proofs. In Proceedings of RTA-95, LNCS 914, pages 426–431, 1995.

    Google Scholar 

  12. B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundam. Informaticae, 24:3–23, 1995.

    Google Scholar 

  13. B. Gramlich. On proving termination by innermost termination. In Proceedings of RTA-96, LNCS 1103, pages 93–107, 1996.

    Google Scholar 

  14. G. Huet and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report 283, INRIA, Le Chesnay, France, 1978.

    Google Scholar 

  15. J.M. Hullot. Canonical forms and unification. In Proceedings of CADE-5, LNCS 87, pages 318–334, 1980.

    Google Scholar 

  16. M.R.K. Krishna Rao. Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science, 151:487–512, 1995.

    Article  Google Scholar 

  17. D.S. Lankford. On proving term rewriting systems are Noetherian. Technical Report Memo MTP-3, Louisiana Technical University, Ruston, LA, 1979.

    Google Scholar 

  18. D.S. Lankford and D.R. Musser. A finite termination criterion, 1978.

    Google Scholar 

  19. A. Middeldorp, H. Ohsaki, and H. Zantema. Transforming termination by self-labelling. In Proceedings of CADE-IS, LNCS 1104, pages 373–387, 1996.

    Google Scholar 

  20. J. Steinbach. Generating polynomial orderings. Inf. Pr. Let., 49:85–93, 1994.

    Google Scholar 

  21. J. Steinbach. Automatic termination proofs with transformation orderings. In Proceedings of RTA-95, LNCS 914, pages 11–25, 1995.

    Google Scholar 

  22. J. Steinbach. Simplification orderings: history of results. Fundamenta Informaticae, 24:47–87, 1995.

    Google Scholar 

  23. H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.

    Article  Google Scholar 

  24. H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Utrecht University, P.O. Box 80.089, 3508, TB Utrecht, The Netherlands

    Thomas Arts

  2. FB Informatik, TH Darmstadt, Alexanderstr. 10, 64283, Darmstadt, Germany

    Jürgen Giesl

Authors
  1. Thomas Arts
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hubert Comon

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arts, T., Giesl, J. (1997). Proving innermost normalisation automatically. In: Comon, H. (eds) Rewriting Techniques and Applications. RTA 1997. Lecture Notes in Computer Science, vol 1232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62950-5_68

Download citation

  • DOI: https://doi.org/10.1007/3-540-62950-5_68

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62950-4

  • Online ISBN: 978-3-540-69051-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation