\begin{frame} \small \begin{block}{Question} How to find suitable polynomials ? \end{block} \bigskip \begin{block}<2->{Modern Approach} \begin{enumerate} \item[(a)]~ choose \alert<2>{abstract} polynomial interpretations (linear, quadratic, \dots) \item[(b)]<3->~ transform rewrite rules into polynomial ordering constraints \item[(c)]<4->~ add monotonicity and well-definedness constraints \item[(d)]<5->~ eliminate universally quantified variables \item[(e)]<6->~ translate resulting constraints to SAT or SMT problem \end{enumerate} \end{block} \end{frame}