A Quantifier Elimination Algorithm for Linear Real Arithmetic
作者： David Monniaux
DOI: 10.1007/978-3-540-89439-1_18
关键词: Conjunctive normal form 、 Elimination theory 、 Satisfiability 、 Mathematics 、 Quantifier elimination 、 Projection (set theory) 、 Modulo 、 Linear inequality 、 Algorithm 、 Disjunctive normal form
摘要: We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This uses as subroutines satisfiability modulo this and polyhedral projection; there are good algorithms implementations both these. The presented in paper is compared, on examples arising from program analysis problems random examples, to several other implementations, all which cannot solve some that our solves easily.
springer.com
arxiv.org
core.ac.uk
archives-ouvertes.fr
sci-hub.st 参考文章(16)
David Pichardie, Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés Rennes 1. ,(2005)
Jean-Louis Imbert, Fourier's Elimination: Which to Choose? PPCP. pp. 117- 129 ,(1993)
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli, DPLL(T): Fast Decision Procedures Computer Aided Verification. pp. 175- 188 ,(2004) , 10.1007/978-3-540-27813-9_14
Alfred Tarski, A decision method for elementary algebra and geometry ,(1951)
David Monniaux, Optimal abstraction on real-valued programs static analysis symposium. pp. 104- 120 ,(2007) , 10.1007/978-3-540-74061-2_7
Quantifier elimination and cylindrical algebraic decomposition Texts and monographs in symbolic computation. ,(1998) , 10.1007/978-3-7091-9459-1
Saugata Basu, Marie-Françoise Roy, Richard Pollack, Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics) Springer-Verlag New York, Inc.. ,(2006)
Aaron R. Bradley, Zohar Manna, The Calculus of Computation : Decision Procedures with Applications to Verification ,(2010)
Leonardo de Moura, Harald Rueß, Maria Sorea, Lazy Theorem Proving for Bounded Model Checking over Infinite Domains conference on automated deduction. pp. 438- 455 ,(2002) , 10.1007/3-540-45620-1_35
Tobias Nipkow, Linear Quantifier Elimination international joint conference on automated reasoning. pp. 18- 33 ,(2008) , 10.1007/978-3-540-71070-7_3