[isabelle-dev] MIR decision procedure

[Lawrence Paulson]

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.

Larry

> 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.