*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals*From*: "Sascha Boehme" <boehmes at in.tum.de>*Date*: Thu, 29 Sep 2016 21:50:04 +0200*Cc*: Manuel Eberl <eberlm at in.tum.de>*In-reply-to*: <57096768.9070101@in.tum.de>*User-agent*: SOGoMail 2.3.11

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. Cheers, Sascha Am Samstag, 09. April 2016 22:34 CEST, Manuel Eberl <eberlm at in.tum.de> 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 >

**Follow-Ups**:**Re: [isabelle] Solving big quantifier-free linear real arithmetic goals***From:*Manuel Eberl

- Previous by Date: [isabelle] New in the AFP: Allen's Interval Calculus
- Next by Date: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals
- Previous by Thread: [isabelle] New in the AFP: Allen's Interval Calculus
- Next by Thread: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list