Proof synthesis and reflection for linear arithmetic (Q945055)

The authors present an implementation of quantifier elimination for integer and linear arithmetic. The algorithms (those by Cooper for \({\mathbb Z}\) and by Ferrante and Rackoff for \({\mathbb R}\)) are realized in two different ways: one \textit{in a tactic style}, by a proof producing a functional program, and the other one \textit{by reflection}, i.e.\ by computations inside the logic. The methods are compared using an implementation in Isabelle/HOL; it is noted that the implementation using the reflective approach is faster.