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



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




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