Skip to Main content Skip to Navigation
New interface
Other publications

A Generalized Framework for Virtual Substitution

Marek Kosta 1, 2 Thomas Sturm 2, 1 
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Other publications
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, December 7, 2015 - 5:37:04 PM
Last modification on : Saturday, February 19, 2022 - 3:08:18 AM

Links full text


  • HAL Id : hal-01239431, version 1
  • ARXIV : 1501.05826



Marek Kosta, Thomas Sturm. A Generalized Framework for Virtual Substitution. 2015, pp.17. ⟨hal-01239431⟩



Record views