Quantifier Elimination for Linear Arithmetic

Title:	Quantifier Elimination for Linear Arithmetic
Author:	Tobias Nipkow
Submission date:	2008-01-11
Abstract:	This article formalizes quantifier elimination procedures for dense linear orders, linear real arithmetic and Presburger arithmetic. In each case both a DNF-based non-elementary algorithm and one or more (doubly) exponential NNF-based algorithms are formalized, including the well-known algorithms by Ferrante and Rackoff and by Cooper. The NNF-based algorithms for dense linear orders are new but based on Ferrante and Rackoff and on an algorithm by Loos and Weisspfenning which simulates infenitesimals. All algorithms are directly executable. In particular, they yield reflective quantifier elimination procedures for HOL itself. The formalization makes heavy use of locales and is therefore highly modular.
BibTeX:	@article{LinearQuantifierElim-AFP, author = {Tobias Nipkow}, title = {Quantifier Elimination for Linear Arithmetic}, journal = {Archive of Formal Proofs}, month = jan, year = 2008, note = {\url{http://isa-afp.org/entries/LinearQuantifierElim.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.