Adam Koprowski, Hans Zantema: Certification of Proving Termination of Term Rewriting by Matrix Interpretations. SOFSEM 2008: 328-339