A Generalized Framework for Virtual Substitution

TL;DR

This paper extends virtual substitution for real quantifier elimination to higher degrees, explicitly representing test points with Thom codes and systematically constructing elimination sets with lower bounds.

Contribution

It generalizes virtual substitution to arbitrary bounded degrees and explicitly details the representation of test points using Thom codes.

Findings

Explicit representation of test points with Thom codes

Systematic construction of elimination sets with lower bounds

Extension of virtual substitution framework to higher degrees

Abstract

We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds.