This tool was developed as bachelor project at Computational Logic group of the University of Innsbruck.
(Polynomial) interpretations are a useful technique to establish termination of term rewrite systems. However, finding suitable polynomials is undecidable and hence challenging. This bachelor project provides a Haskell program that evaluates a given (polynomial) interpretation on a given rewrite system and checks compatibility and monotonicity on the base of a sufficient criterion. The program supports non-linear polynomial and matrix interpretations.