An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations.

Ahlem Ben Cherifa, Pierre Lescanne

Browse the full CADE paper archive.