Linear Quantifier Elimination
This paper presents verified quantifier elimination procedures for
dense linear orders (DLO), for real and for integer linear arithmetic.
The DLO procedures are new. All procedures are defined and verified in
the theorem prover Isabelle/HOL, are executable and can be applied to
HOL formulae themselves (by reflection).
pdf
BibTeX:
@inproceedings{Nipkow-IJCAR08,author={Tobias Nipkow},
title={Linear Quantifier Elimination},
booktitle={Automated Reasoning (IJCAR 2008)},
editor={A. Armando and P. Baumgartner and G. Dowek},publisher={Springer},
series={LNCS},volume={5195},pages={18-33},year=2008}
Isabelle theories in the
Archive of Formal Proofs