We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with -∞,with the operations ”max” and ”plus”. This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the Dependency Pairs transformation, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers ”below zero”: integers extended with -∞.This allows to treat some termination problems with symbols that require a predecessor semantics. The contents of the paper has been formally verified in the
proof assistant and the formalization has been contributed to the
library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method. We also report on experiments with an implementation of this method which, compared to results from 2007, outperforms
(winner of the certified termination competition for term rewriting), and in the string rewriting category is as powerful as
was but now all of the proofs are certified.