Email Gateway (Aug 18 2022 at 12:07): Email Gateway (Aug 18 2022 at 12:07):From: Amine Chaieb <chaieb@in.tum.de>
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
Last updated: May 03 2024 at 12:27 UTC