[isabelle-dev] MIR decision procedure

Lawrence Paulson lp15 at cam.ac.uk
Tue Dec 1 18:23:03 CET 2015

We now have presburger as a stand-alone proof method. Possibly the other procedures could be bundled into that. There are times when it is definitely worth the wait.


> On 1 Dec 2015, at 16:14, Amine Chaieb <amine at chaieb.org> wrote:
> 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.

More information about the isabelle-dev mailing list