Proving innermost normalisation automatically
- 1 January 1997
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 157-171
- https://doi.org/10.1007/3-540-62950-5_68
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.Keywords
This publication has 12 references indexed in Scilit:
- Automatically proving termination where simplification orderings failPublished by Springer Science and Business Media LLC ,1997
- Modular proofs for completeness of hierarchical term rewriting systemsTheoretical Computer Science, 1995
- Natural terminationTheoretical Computer Science, 1995
- SIMPLIFICATION ORDERINGS: HISTORY OF RESULTSFundamenta Informaticae, 1995
- ABSTRACT RELATIONS BETWEEN RESTRICTED TERMINATION AND CONFLUENCE PROPERTIES OF REWRITE SYSTEMSFundamenta Informaticae, 1995
- Generating polynomial orderingsInformation Processing Letters, 1994
- Termination by completionApplicable Algebra in Engineering, Communication and Computing, 1990
- Termination of rewriting systems by polynomial interpretations and its implementationScience of Computer Programming, 1987
- Termination of rewritingJournal of Symbolic Computation, 1987
- A note on simplification orderingsInformation Processing Letters, 1979