A Generalized Framework for Virtual Substitution

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.
Type de document :
Autre publication
preprint. 2015, pp.17
Liste complète des métadonnées

https://hal.inria.fr/hal-01239431
Contributeur : Stephan Merz <>
Soumis le : lundi 7 décembre 2015 - 17:37:04
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Identifiants

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

Collections

Citation

Marek Kosta, Thomas Sturm. A Generalized Framework for Virtual Substitution. preprint. 2015, pp.17. 〈hal-01239431〉

Partager

Métriques

Consultations de la notice

95