{"content":[{"text":"Quantiﬁer Elimination (QE) by Virtual Substitution","bbox":{"left":0.023438,"top":0.024145,"width":0.9381070000000001,"height":0.066215}},{"text":"Input: First order formula ∃xϕ \n Output: Quantiﬁer-free formula ϕ′ with","bbox":{"left":0.090198,"top":0.208953,"width":0.516724,"height":0.1124}},{"text":"∃xϕ ←→ ϕ′ \n General idea: Compute an elimination set E, such that \n � \n ∃xϕ ←→ (γ ∧ ϕ[t//x]) \n (γ,t)∈E \n For the reals and for the integers: Elements of elimination sets \n are built essentially from interval boundaries","bbox":{"left":0.090198,"top":0.358625,"width":0.8633770000000001,"height":0.42055199999999987}},{"text":"A. Lasaruk, T. Sturm","bbox":{"left":0.03299,"top":0.967468,"width":0.158898,"height":0.027590000000000003}},{"text":"(Uni Passau)","bbox":{"left":0.201049,"top":0.967468,"width":0.09929299999999999,"height":0.027590000000000003}},{"text":"WQE for the Integers","bbox":{"left":0.41827,"top":0.967468,"width":0.163445,"height":0.027590000000000003}},{"text":"December 4, 2007","bbox":{"left":0.764516,"top":0.967468,"width":0.13919500000000007,"height":0.027590000000000003}},{"text":"2 / 25","bbox":{"left":0.94124,"top":0.967468,"width":0.041220000000000034,"height":0.027590000000000003}}],"images_bbox":[{"left":0.057878,"top":0.220486,"width":0.019293,"height":0.029398},{"left":0.057878,"top":0.282957,"width":0.019293,"height":0.025723},{"left":0.057878,"top":0.463021,"width":0.019293,"height":0.025723},{"left":0.057878,"top":0.694531,"width":0.019293,"height":0.025723}],"images_bbox_not_text_overlap":[{"left":0.057878,"top":0.220486,"width":0.019293,"height":0.029398},{"left":0.057878,"top":0.282957,"width":0.019293,"height":0.025723},{"left":0.057878,"top":0.463021,"width":0.019293,"height":0.025723},{"left":0.057878,"top":0.694531,"width":0.019293,"height":0.025723}]}