English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. View item / 
  2. Item Summary

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Paper

A Generalized Framework for Virtual Substitution

MPS-Authors
/persons/resource/persons127668

Košta,  Marek
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons73108

Sturm,  Thomas       
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1501.05826.pdf
(Preprint), 469KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Košta, M., & Sturm, T. (2015). A Generalized Framework for Virtual Substitution. Retrieved from http://arxiv.org/abs/1501.05826.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0024-A3C1-0
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.