[isabelle-dev] MIR decision procedure
nipkow at in.tum.de
Fri Nov 13 17:18:56 CET 2015
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.
On 13/11/2015 17:05, Lawrence Paulson wrote:
> The MIR decision procedure is again working. We still have the mystery of what it is good for. It is not used anywhere at all. Even the test suite consists of a mere five problems. And I have now stumbled across ferrack. It seems to be used quite a bit, but what does it do? Is it documented anywhere?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev