Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems

DOI10.1007/978-3-540-88282-4_30zbMath1156.68430MaRDI QIDQ3540124

Aart Middeldorp, Martin Korp

Publication date: 20 November 2008

Published in: Language and Automata Theory and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-88282-4_30

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q42: Grammars and rewriting systems

Related Items

Beyond Dependency Graphs, Match-bounds revisited

Uses Software

• Tyrolean
• Matchbox

Cites Work

• Unnamed Item
• Unnamed Item
• Termination of string rewriting proved automatically
• Termination proofs for string rewriting systems via inverse match-bounds
• Tyrolean termination tool: techniques and features
• On tree automata that certify termination of left-linear term rewriting systems
• Mechanizing and improving dependency pairs
• Decidability for left-linear growing term rewriting systems.
• Match-bounded string rewriting systems
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Proving Termination of Rewrite Systems Using Bounds
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Frontiers of Combining Systems
• Term Rewriting and Applications
• Logic for Programming, Artificial Intelligence, and Reasoning