*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 30 Sep 2016 08:06:54 +0200*In-reply-to*: <753e-57ed7080-6f-6552df80@74870949>*References*: <753e-57ed7080-6f-6552df80@74870949>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Hallo Sascha, very nice indeed! I shall take a look at it. I've since converted the SMT-based proof into a fully-structured Isar proof (which was my goal anyway, I just wasn't sure whether it was feasible â it was) Still, I'm sure this will be very useful if I ever run into similar issues in the future. Cheers, Manuel On 29/09/16 21:50, Sascha Boehme wrote: > 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 >> > > > > > > >

**References**:**Re: [isabelle] Solving big quantifier-free linear real arithmetic goals***From:*Sascha Boehme

- Previous by Date: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals
- Next by Date: [isabelle] Problems with Code-Generator
- Previous by Thread: Re: [isabelle] Solving big quantifier-free linear real arithmetic goals
- Next by Thread: [isabelle] Problems with Code-Generator
- 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