Proof Synthesis and Reflection for Linear Arithmetic

Amine Chaieb and Tobias Nipkow

This article presents detailed implementations of quantifier elimination for both integer and real linear arithmetic for theorem provers. The underlying algorithms are those by Cooper (for Z) and by Ferrante and Rackoff (for R). Both algorithms are realized in two entirely different ways: once in tactic style, i.e. by a proof-producing functional program, and once by reflection, i.e. by computations inside the logic rather than in the meta-language. Both formalizations are highly generic because they make only minimal assumptions w.r.t. the underlying logical system and theorem prover. An implementation in Isabelle/HOL shows that the reflective approach is between one and two orders of magnitude faster.



@article{ChaiebN-JAR08,author={Amine Chaieb and Tobias Nipkow},
title={Proof Synthesis and Reflection for Linear Arithmetic},
journal={J. Automated Reasoning},volume=41,pages={33--59},year=2008}

This paper is a completely revised and extended version of this technical report.