### 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.

### License

BSD License

### Topics

- Logic/General logic/Decidability of theories

### Related publications

- Nipkow, T. (2010). Linear Quantifier Elimination. Journal of Automated Reasoning, 45(2), 189–212. https://doi.org/10.1007/s10817-010-9183-0
- author's copy

### Session LinearQuantifierElim

- Logic
- QE
- DLO
- QEdlo
- QEdlo_ex
- QEdlo_fr
- QEdlo_inf
- LinArith
- QElin
- QElin_opt
- FRE
- QElin_inf
- PresArith
- QEpres
- Cooper
- CertDlo
- CertLin

## Cite

×

LinearQuantifierElim-AFP

    @article{LinearQuantifierElim-AFP,
      author  = {Tobias Nipkow},
      title   = {Quantifier Elimination for Linear Arithmetic},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2008},
      note    = {\url{https://isa-afp.org/entries/LinearQuantifierElim.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Feb 12, 2008 : Isabelle2007
- Jan 24, 2008 : Isabelle2007
- Jan 11, 2008 : Isabelle2007