Email Gateway (Aug 18 2022 at 11:17): Email Gateway (Aug 18 2022 at 11:17):From: Tobias Nipkow <nipkow@in.tum.de>
The following article has recently made it into the the Archive of
Formal Proofs:
Quantifier Elimination for Linear Arithmetic
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.
Enjoy
Tobias
Email Gateway (Aug 18 2022 at 11:17):From: Tobias Nipkow <nipkow@in.tum.de>
PS A paper describing parts of the development is available here:
http://www.in.tum.de/~nipkow/pubs/MOD2007.html
Tobias
Last updated: Oct 31 2025 at 08:28 UTC