SMT-based synthesis of certified termination proofs

Abstract - Polynomial orders are a popular technique
for showing termination of term rewrite systems.
The automated search for suitable polynomials
often boils down to non-linear constraints for which
SAT modulo theory is not decidable.
Therefore we integrated a technique into AProVE that converts non-linear
polynomial constraints into linear ones. Here we first restrict the
search space to a finite fragment to render the problem decidable.
Afterwards, we benefit from this information to abstract non-linear
monomials to intermediate variables, whose value is then fixed by case
analysis on the input variables. In the end, we obtain an SMT problem
for linear arithmetic which we then solve by an off-the-shelf SMT solver.

Additionally we introduced the transformation of exported
proofs into a new common format for certification of termination
proofs by trusted proof assistants like Isabelle or Coq and
were able to participate and win in 3 of 4 certified categories
of the last termination competition on term rewriting.