Proving a specific type of inequality theorems in ACL2
Hanbing Liu · 2009
We describe how we guide ACL2 to follow a divide-andconquer strategy for proving inequalities of the type |P(e)| ≤ C. P(e) is a polynomial in variables e and C is a constant.Our approach involves (1) writing an ACL2 program to estimate the upper-bound of such polynomials and (2) using the bind-free mechanism to integrate the upper-bound estimation program to guide rewriting. We think it is interesting to showcase how we extract the relevant information from the hypothesis and how such information is used to influence rewriting.Techniques like ours can be useful to ACL2 users who want to better control rewriting when their problems share specific characteristics with our |P(e)| ≤ C type problem.