Linear Quantifier Elimination

Tobias Nipkow

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

This paper has been superseded by an extended journal version.