Reflecting Quantifier Elimination for Linear Arithmetic

Tobias Nipkow

This paper formalizes and verifies quantifier elimination procedures for dense linear orders and for real and integer linear arithmetic in the theorem prover Isabelle/HOL. It is a reflective formalization because it can be applied to HOL formulae themselves. In particular we obtain verified executable decision procedures for linear arithmetic. The formalization for the various theories is modularized with the help of locales, a structuring facility in Isabelle.

pdf

BibTeX:

@inproceedings{Nipkow-MOD2007,author={Tobias Nipkow},
title={Reflecting Quantifier Elimination for Linear Arithmetic},
booktitle={Formal Logical Methods for System Security and Correctness},
publisher={IOS Press},editor={O. Grumberg and T. Nipkow and C. Pfaller},
pages = {245--266},year=2008}

Isabelle theories in the Archive of Formal Proofs