Re: [isabelle] Solving big quantifier-free linear real arithmetic goals

Hi Manuel,

You might be interested to hear that the next Isabelle release will provide a new method named argo that is capable of solving such goals without invoking an external tool. With argo, your goals can be proved within five seconds on off-the-shelf hardware.


Am Samstag, 09. April 2016 22:34 CEST, Manuel Eberl <eberlm at> schrieb:

> Hallo,
> I am currently working on some Social Choice Theory. The proof basically
> works by deriving a number of equalities and inequalities over real

> numbers and then showing that they are inconsistent.
> I have already derived these conditions and now need to show that they
> are actually inconsistent. This is goal1 in the attachment. Here, pmf is
> from HOL-Probability and sds, R1, R2, a, b, c, d etc. are
> constants/fixed locale variables whose properties are irrelevant for 
> this goal. To emphasise this: I can restate the goal by generalising it
> a bit, introducing real variables for all the expressions (see goal2).
> If one simplifies this a bit and eliminates redundant variables, one 
> obtains goal3.
> I tried the following things:
> â smt (i.e. Z3) is able to solve goal1 within .3 seconds; proof
> reconstruction takes another 12 seconds.
> â smt solves goal2 within .5 seconds; proof reconstruction seems to take
> longer than my patience will permit though.
> â smt solves goal3 within .3 seconds; proof reconstruction takes 67 seconds.
> â Both goals should be solvable by linarith in theory. I tried it and
> gave up after an hour or so.
> This raises the following questions:
> â Why is this trivial for Z3 but impossible for linarith?
> â Is there any hope of tweaking linarith to get this proof through?
> â Why does proof reconstruction take so much longer on goal2 and goal3,
> even though they are arguably âsimplerâ?
> I know that proofs using smt are not allowed in the AFP, so the prospect
> that I can only prove this with smt is a bit troubling.
> Incidentally, another question: Is there any easy way to turn something
> like goal1 into something like goal2, i.e. generalise all real
> non-literals in a term to real variables? I wrote my own very ad-hoc 
> tactic for this, but it seems like quite a common use case.
> Cheers,
> Manuel

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.