[isabelle-dev] MIR decision procedure

[Amine Chaieb]

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.

PS: Feerack is quantifier elimination over linear arithmetic (although I
had at some point quite relaxed conditions so it can work inside any dense
linear order with a between "picker", i.e. a function that given l and u
st. l<u in the DLO, it would pick an x s.t. l<x<u)

On Fri, November 13, 2015 12:28 pm, Lawrence Paulson wrote:
> But couldn’t these procedures be included in linarith, or at least in
> “try”?
> Larry
>
>
>> 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.
>>
>
> _______________________________________________
> isabelle-dev mailing list isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d
> ev
>