Induction for termination with local strategies

DOI10.1016/S1571-0661(04)00284-1zbMath1268.68146OpenAlexW2094830274MaRDI QIDQ2841240

Olivier Fissore, Hélène Kirchner, Isabelle Gnaedig

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)00284-1

zbMATH Keywords

rewritinginductionterminationnarrowingrule-based languagesordering constraintslocal strategy on operators

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Unnamed Item, Unnamed Item, Proving weak properties of rewriting, Applications and extensions of context-sensitive rewriting, Induction for termination with local strategies, Modular and incremental automated termination proofs, ELAN from a rewriting logic point of view

Uses Software

• Stratego
• ELAN
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Completeness results for basic narrowing
• Some characteristics of strong innermost normalization
• Context-sensitive rewriting strategies
• Induction for termination with local strategies
• Proving innermost normalisation automatically
• Termination of context-sensitive rewriting