Termination of string rewriting proved automatically

DOI10.1007/s10817-005-6545-0zbMath1102.68649OpenAlexW1970844917MaRDI QIDQ850497

Hans Zantema

Publication date: 3 November 2006

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-005-6545-0

zbMATH Keywords

terminationstring rewritingrelative terminationmatch-boundssemantic labelling

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Termination of string rewriting proved automatically ⋮ Lower bounds for runtime complexity of term rewriting ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Mechanizing and improving dependency pairs ⋮ Deciding Innermost Loops ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Adding constants to string rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Unnamed Item ⋮ A non-termination criterion for binary constraint logic programs ⋮ An automated approach to the Collatz conjecture ⋮ Loops under Strategies ⋮ Match-bounds revisited ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM

Uses Software

• AProVE
• CiME
• Matchbox
• Tsukuba
• TORPA
• REVE

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Orderings for term-rewriting systems
• Termination of string rewriting proved automatically
• On recursive path ordering
• Termination of term rewriting: Interpretation and type elimination
• Match-bounded string rewriting systems
• Termination of term rewriting using dependency pairs
• The 3x + 1 Problem and Its Generalizations
• Non-Looping String Rewriting
• Mathematical Foundations of Computer Science 2003
• Implementation and Application of Automata
• Rewriting Techniques and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item