Proof Synthesis and Reflection for Linear Arithmetic
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.
pdf
BibTeX:
@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.