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.