@inproceedings{Mon08c,
title = { A Quantifier Elimination Algorithm for Linear Real Arithmetic },
author = {Monniaux, David},
year = {2008},
booktitle = {LPAR (Logic for Programming Artificial Intelligence and Reasoning)},
pages = {243-257},
publisher = {Springer Verlag},
series = {Lecture Notes in Computer Science},
volume = {5330},
team = {SYNC,PACSS},
pdf = {http://www-verimag.imag.fr/~monniaux/biblio/Monniaux_LPAR08.pdf},
abstract = {We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutines satisfiability modulo this theory and polyhedral projection; there are good algorithms and implementations for both of these. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems and on random examples, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily. },
}
