Improving Automated Strategies for Univariate Quantifier Elimination
This report discusses improved support for univariate quantifier elimination in the Prototype Verification System (PVS). Previously, PVS had three strategies for quantifier elimination—hutch, tarski, and sturm. Of these, only hutch is able to decide queries in any input format—sturm only works on queries regarding a single polynomial on an interval and tarski resolves queries in the universal existential fragment. This paper describes an extended version of tarski. The extension is accomplished by formally verifying a disjunctive normal form transformation in PVS and using tarski on each conjunctive clause. Additionally, a preprocessing step is added to the decision procedure underlying tarski. This preprocessing is designed to exploit properties of polynomial structure to quickly resolve queries that have certain formats. The preprocessing produces dramatic speedup when it succeeds in resolving a query, and seems to introduce negligible overhead when it does not resolve a query. Finally, testing reveals some ways to improve the hutch and tarski strategies.