Matrix interpretations for proving termination of term rewriting

J. Endrullis, J. Waldmann, H. Zantema

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

10 Citaten (Scopus)
2 Downloads (Pure)


We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.
Originele taal-2Engels
TitelAutomated reasoning : 3rd international joint conference, IJCAR'06, Seattle WA, USA, August 17-20, 2006 : proceedings
RedacteurenU. Furbach, N. Shankar
Plaats van productieBerlin
ISBN van geprinte versie3-540-37187-7
StatusGepubliceerd - 2006

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

Citeer dit