K. Decidability-results-over, MaxPoly{K} and MaxPlus{K} In this section, we review the results of the DPI synthesis problem

N. D. Jones, Computability and Complexity from a Programming Perspective, 1997.
DOI : 10.1007/978-94-010-0413-8_4

T. Arts and J. , Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

D. Lankford, On proving term rewriting systems are noetherian, Tech. rep, 1979.

Z. Manna and S. Ness, On the termination of Markov algorithms, Third hawaii international conference on system science, pp.789-792, 1970.

E. Cichon and P. Lescanne, Polynomial interpretations and the complexity of algorithms, pp.139-147, 1992.
DOI : 10.1007/3-540-55602-8_161

D. Hofbauer and C. Lautemann, Termination proofs and the length of derivations (preliminary version, LNCS, vol.355, pp.167-177, 1989.

G. Moser and A. Schnabl, Proving Quadratic Derivational Complexities Using Context Dependent Interpretations, LNCS, vol.5117, pp.276-290, 2008.
DOI : 10.1007/978-3-540-70590-1_19

J. Marion and J. Moyen, Efficient first order functional program interpreter with time bound certifications, LNCS, vol.1955, pp.25-42, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099178

G. Bonfante, J. Marion, and J. Moyen, On Lexicographic Termination Ordering with Space Bound Certifications, LNCS, vol.2244, pp.482-493, 2001.
DOI : 10.1007/3-540-45575-2_46
URL : https://hal.archives-ouvertes.fr/inria-00100523

G. Bonfante, J. Marion, and J. Moyen, Quasi-interpretations and Small Space Bounds, LNCS, vol.3467, pp.150-164, 2005.
DOI : 10.1007/978-3-540-32033-3_12
URL : https://hal.archives-ouvertes.fr/inria-00001234

J. Marion and R. Péchoux, Characterizations of polynomial complexity classes with a better intensionality, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.79-88, 2008.
DOI : 10.1145/1389449.1389460
URL : https://hal.archives-ouvertes.fr/inria-00332389

R. Amadio, Synthesis of max-plus quasi-interpretations, Fundamenta Informaticae, vol.65, issue.12
URL : https://hal.archives-ouvertes.fr/hal-00146968

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-kamp, R. Thiemann et al., SAT Solving for Termination Analysis with Polynomial Interpretations, LNCS, pp.340-354, 2007.
DOI : 10.1007/978-3-540-72788-0_33

C. Borralleras, S. Lucas, A. Oliveras, E. Rodríguez-carbonell, and A. Rubio, SAT Modulo Linear Arithmetic for Solving Polynomial Constraints, Journal of Automated Reasoning, vol.207, issue.2, pp.107-131, 2012.
DOI : 10.1007/s10817-010-9196-8

M. Avanzini, G. Moser, and A. Schnabl, Automated Implicit Computational Complexity Analysis (System Description), LNCS, vol.5195, pp.132-138, 2008.
DOI : 10.1007/978-3-540-71070-7_10

G. Bonfante, J. Marion, and R. Péchoux, Quasi-interpretation Synthesis by Decomposition, LNCS, vol.4711, pp.410-424, 2007.
DOI : 10.1007/978-3-540-75292-9_28
URL : https://hal.archives-ouvertes.fr/inria-00130920

S. Kleene, Introduction to metamathematics, Wolters-Noordhoff, 1988.

N. Dershowitz, A note on simplification orderings, Information Processing Letters, vol.9, issue.5, pp.212-215, 1979.
DOI : 10.1016/0020-0190(79)90071-1

S. Lucas, On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting, Applicable Algebra in Engineering, Communication and Computing, vol.17, issue.1, pp.49-73, 2006.
DOI : 10.1007/s00200-005-0189-5

E. Contejean, C. Marché, A. Tomás, and X. Urbain, Mechanically Proving Termination Using Polynomial Interpretations, Journal of Automated Reasoning, vol.12, issue.1, pp.325-363, 2005.
DOI : 10.1007/s10817-005-9022-x
URL : https://hal.archives-ouvertes.fr/inria-00001167

S. Lucas, Practical use of polynomials over the reals in proofs of termination, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, PPDP '07, pp.39-50, 2007.
DOI : 10.1145/1273920.1273927

F. Neurauter and A. Middeldorp, Polynomial interpretations over the reals do not subsume polynomial interpretations over the integers, pp.243-258, 2010.

Y. V. Matiyasevich, Hilbert's 10th Problem, Foundations of Computing Series, 1993.

A. Tarski, A Decision Method for Elementary Algebra and Geometry, 1951.
DOI : 10.1007/978-3-7091-9459-1_3

G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Conference on Automata Theory and Formal Languages, 1975.

G. Bonfante, J. Marion, and J. Moyen, Quasi-interpretations a way to control resources, Theoretical Computer Science, vol.412, issue.25, pp.2776-2796, 2011.
DOI : 10.1016/j.tcs.2011.02.007
URL : https://hal.archives-ouvertes.fr/hal-00591862

Y. Matiyasevich and M. Davis, Hilbert's tenth problem, 1993.

A. Weiermann, Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science, vol.139, issue.1-2, pp.355-362, 1995.
DOI : 10.1016/0304-3975(94)00135-6

G. Bonfante, A. Cichon, J. Marion, and H. Touzet, Algorithms with polynomial interpretation termination proof, Journal of Functional Programming, vol.11, issue.1, pp.33-53, 2001.
DOI : 10.1017/S0956796800003877
URL : https://hal.archives-ouvertes.fr/inria-00100819

J. Endrullis, J. Waldmann, and H. Zantema, Matrix Interpretations for Proving Termination of Term Rewriting, Journal of Automated Reasoning, vol.17, issue.4, pp.195-220, 2008.
DOI : 10.1007/s10817-007-9087-9

J. Waldmann, Polynomially bounded matrix interpretations, pp.357-372, 2010.

F. Neurauter, H. Zankl, and A. Middeldorp, Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting, LPAR (Yogyakarta ), pp.550-564, 2010.
DOI : 10.1007/978-3-642-16242-8_39

G. Moser, A. Schnabl, and J. Waldmann, Complexity analysis of term rewriting based on matrix and context dependent interpretations, FSTTCS, vol.2, pp.304-315, 2008.

A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. , Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems, LNCS, vol.88, issue.2, pp.1-20, 2011.
DOI : 10.1007/978-3-642-17511-4_27

D. Hofbauer, Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Theoretical Computer Science, vol.105, issue.1, pp.129-140, 1992.
DOI : 10.1016/0304-3975(92)90289-R
URL : http://doi.org/10.1016/0304-3975(92)90289-r

M. S. Krishnamoorthy and P. Narendran, On recursive path ordering, Theoretical Computer Science, vol.40, issue.2-3, pp.323-328, 1985.
DOI : 10.1016/0304-3975(85)90175-6

N. Hirokawa and G. Moser, Automated Complexity Analysis Based on the Dependency Pair Method, LNCS, vol.5195, pp.364-379, 2008.
DOI : 10.1007/978-3-540-71070-7_32

J. Marion and R. Péchoux, Analyzing the implicit computational complexity of object-oriented programs, pp.316-327, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332550