Proof Synthesis and Reflection for Linear Arithmetic

13 years 7 months ago
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 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.
Amine Chaieb, Tobias Nipkow
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JAR
Authors Amine Chaieb, Tobias Nipkow
Comments (0)