Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

DOI10.4230/LIPIcs.RTA.2011.251zbMath1236.68141OpenAlexW2160428591MaRDI QIDQ5389085

Aart Middeldorp, Friedrich Neurauter

Publication date: 24 April 2012

Full work available at URL: http://subs.emis.de/LIPIcs/frontdoor_4903.html

zbMATH Keywords

terminationterm rewritingmatrix interpretations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Automatic synthesis of logical models for order-sorted first-order theories, An automated approach to the Collatz conjecture, Use of Logical Models for Proving Operational Termination in General Logics, Derivational complexity and context-sensitive Rewriting

Uses Software

• Chaff