[isabelle-dev] MIR decision procedure
lp15 at cam.ac.uk
Fri Nov 13 19:28:13 CET 2015
But couldn’t these procedures be included in linarith, or at least in “try”?
> On 13 Nov 2015, at 16:18, Tobias Nipkow <nipkow at 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.
More information about the isabelle-dev