Proving innermost normalisation automatically

DOI10.1007/3-540-62950-5_68MaRDI QIDQ4594225zbMATH OpenOpenAlexFDO

Authors Thomas Arts, Jürgen Giesl

Publication date 17 November 2017

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://dspace.library.uu.nl/handle/1874/18360

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Termination of term rewriting using dependency pairs
• On proving termination by innermost termination
• Some characteristics of strong innermost normalization
• Normalization properties for shallow TRS and innermost rewriting
• Deciding Innermost Loops

Cited in

(13)

• Some characteristics of strong innermost normalization
• ELAN from a rewriting logic point of view
• Termination of term rewriting using dependency pairs
• Using well-founded relations for proving operational termination
• Compact normalisation trace via lazy rewriting
• Induction for termination with local strategies
• Outermost ground termination
• Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
• Usable Rules for Context-Sensitive Rewrite Systems
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Termination of Priority Rewriting
• Proving weak properties of rewriting
• Context-sensitive dependency pairs

This page was built for publication: Proving innermost normalisation automatically

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4594225)