A Quantifier Elimination Algorithm for Linear Real Arithmetic

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily.
accepted at LPAR '08

Keywords

Logic in Computer Science

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/168254

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0803.1575
 http://arxiv.org/abs/0803.1575

Collections

arXiv