NTRS - NASA Technical Reports Server

Back to Results
Improving Automated Strategies for Univariate Quantifier EliminationThis 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.
Document ID
Acquisition Source
Langley Research Center
Document Type
Technical Memorandum (TM)
Katherine Cordwell
(Carnegie Mellon University Pittsburgh, Pennsylvania, United States)
Cesar A Munoz
(Langley Research Center Hampton, Virginia, United States)
Aaron M Dutle
(Langley Research Center Hampton, Virginia, United States)
Date Acquired
November 24, 2020
Publication Date
January 1, 2021
Subject Category
Computer Programming And Software
Report/Patent Number
Funding Number(s)
WBS: 340428.
Distribution Limits
Public Use Permitted.
Technical Review
Single Expert
Polynomial Constraints
Quantifier Elimination
Prototype Verification System (PVS)
Automated Strategies
No Preview Available