| Abstract: | This paper presents a new look at Weispfenning's 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. |