Re: [isabelle-dev] MIR decision procedure

[Tobias Nipkow]

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.

Tobias

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?

Larry

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev