On Quantifer Elimination by Virtual Term Substitution
NAVAL ACADEMY ANNAPOLIS MD DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
This paper presents a new look at Weispfennings method of quantifier elimination by virtual term substitution and provides two important improvements. Virtual term substitution eliminates a quantified variable by substituting formulas in the remaining variables for each atomic formula in which the quantified variable appears. This paper investigates the polynomials that arise in substitution formulas Weispfenning proposed and, based on this examination, provides a simpler substitution for the general case, and alternate substitutions for several commonly occurring situations. Providing alternate substitutions allows virtual term substitution to make choices that produce simpler output.
- Numerical Mathematics