At the time we decided against it due to the following: By design arith has to solve its goal or fail fast otherwise. Quantifier Elimination is just the opposite of both, since its is in its general form a conversion, and also due to very hard complexity costs (in particular for this MIR theory) cannot generally fail fast.
For the same reason we did not have presburger, or ferrack or the other procedures (from my thesis) inside arith. Amine. PS: Feerack is quantifier elimination over linear arithmetic (although I had at some point quite relaxed conditions so it can work inside any dense linear order with a between "picker", i.e. a function that given l and u st. l<u in the DLO, it would pick an x s.t. l<x<u) On Fri, November 13, 2015 12:28 pm, Lawrence Paulson wrote: > But couldnt these procedures be included in linarith, or at least in > try? > Larry > > >> On 13 Nov 2015, at 16:18, Tobias Nipkow <nip...@in.tum.de> wrote: >> >> >> MIR is "documented" in Amine's IJCAR 2006 paper "Verifying Mixed >> Real-Integer Quantifier Elimination". Maybe the title gives you a hint >> what it is good for. Ferrack stands for Ferrante & Rackoff, who >> invented this QE algorithm. This one may only be "documented" in >> Amine's PhD. >> > > _______________________________________________ > isabelle-dev mailing list isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d > ev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
