[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Incremental termination proofs and the length of derivations

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

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

Included in the following conference series:

Abstract

Incremental termination proofs, a concept similar to termination proofs by quasi-commuting orderings, are investigated. In particular, we show how an incremental termination proof for a term rewriting system T can be used to derive upper bounds on the length of derivations in T. A number of examples show that our results can be applied to yield (sharp) low-degree polynomial complexity bounds.

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

Access this chapter

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. L. Bachmair, N. Dershowitz: Commutation, transformation, and termination. Proc. 8th Conf. on Automated Deduction, LNCS 230, pp. 5–20.

    Google Scholar 

  2. G. Bauer, F. Otto: Finite complete rewriting systems and the complexity of the word problem. Acta Informatica 21, pp. 521–540.

    Google Scholar 

  3. Ph. le Chenadec: Canonical Forms in Finitely Presented Algebras. J. Wiley & Sons

    Google Scholar 

  4. A. Ben Cherifa, P. Lescanne: Termination of Rewriting Systems by Polynomial Interpretations and its Implementation. Sci. of Comp. Prog. 9, pp. 137–159.

    Google Scholar 

  5. N. Dershowitz: Orderings for Term-rewriting systems. TCS 17, pp. 279–301.

    Google Scholar 

  6. N. Dershowitz: Termination of rewriting. J. Symbolic Computation 3, pp. 69–116.

    Google Scholar 

  7. N. Dershowitz, Jean-Pierre Jouannaud: Rewrite systems. Rapport de Recherche no 478, Université de Paris-Sud.

    Google Scholar 

  8. F. Drewes, C. Lautemann: Incremental Termination Proofs and the Length of Derivations. Universität Bremen, report 7/90.

    Google Scholar 

  9. H. Ehrig, B. Mahr: Complexity of Implementations on the Level of Algebraic Specifications. Proc. ACM Symp. Theory of Computing.

    Google Scholar 

  10. D. Hofbauer, C. Lautemann: Termination proofs and the length of derivations. Proc. 3rd Intern. Conf. on Rewriting Techn. and Appl., LNCS 355, pp. 167–177.

    Google Scholar 

  11. G. Huet, D. Oppen: Equations and rewrite rules: a survey. In Ronald V. Book, Ed.: Formal languages, perspectives and open problems, Academic Press.

    Google Scholar 

  12. D. E. Knuth, P. B. Bendix: Simple Word Problems in Universal Algebras. In: J. Leech, Ed.: Computational Problems in Abstract Algebra, Oxford, Pergamon Press.

    Google Scholar 

  13. J.-W. Klop: Term Rewriting Systems: A Tutorial, EATCS Bulletin 32, pp. 143.

    Google Scholar 

  14. D. Lankford: Canonical algebraic simplification in computational logic. Report ATP-25, University of Texas.

    Google Scholar 

  15. Dallas Lankford: On proving term rewriting systems are Noetherian. Report MTP-3, Louisiana Tech University.

    Google Scholar 

  16. J. Steinbach: Extension and comparison of simplification orderings. Proc. 3rd Intern. Conf. on Rewriting Techniques and Applications, LNCS 355, pp. 434–448.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Ronald V. Book

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Drewes, F., Lautemann, C. (1991). Incremental termination proofs and the length of derivations. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_85

Download citation

  • DOI: https://doi.org/10.1007/3-540-53904-2_85

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53904-9

  • Online ISBN: 978-3-540-46383-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics