Title:On Quantifer Elimination by Virtual Term Substitution
Authors:Brown, Christopher W.
Serial Number:2005-07
Publication Date:8-24-2005
Abstract:This paper presents a new look at Weispfenning's method of quantifer elimination by virtual term substitution and provides two important improvements. Virtual term substitution eliminates a quantifed variable by substituting formulas in the remaining variables for each atomic formula in which the quantifed 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 situtions. Providing alternate substitutions allows virtual term substitution to make choices that produce simpler output.
View ReportView bibtex