TY - JOUR
T1 - Matrix Interpretations for Proving Termination of Term Rewriting
AU - Endrullis, J.
AU - Waldmann, J.
AU - Zantema, H.
N1 - 1355864
PY - 2008
Y1 - 2008
N2 - 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 everyrewrite step causes a decrease, but instead of the usual natural numbers we usevectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. Thismethod allows us to prove termination and relative termination. A modification ofthe latter, in which strict steps are only allowed at the top, turns out to be helpful incombination 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-ofthe- art SAT solver. © Springer Science + Business Media B.V. 2007.
AB - 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 everyrewrite step causes a decrease, but instead of the usual natural numbers we usevectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. Thismethod allows us to prove termination and relative termination. A modification ofthe latter, in which strict steps are only allowed at the top, turns out to be helpful incombination 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-ofthe- art SAT solver. © Springer Science + Business Media B.V. 2007.
U2 - 10.1007/s10817-007-9087-9
DO - 10.1007/s10817-007-9087-9
M3 - Article
SN - 0168-7433
VL - 40
SP - 195
EP - 220
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 2-3
ER -