[isabelle] Paper Announcement

Dear all,
We would like to announce a new paper "Proof Synthesis and Reflection for Linear Arithmetic" at JAR (see http://dx.doi.org/10.1007/s10817-008-9101-x). Please contact us if you have any comment or suggestion.

Abstract: 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.

Keywords:  Proof synthesis - Reflection - Linear arithmetic

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.