[isabelle-dev] Presburger proof term

[amine at chaieb.org]

The good/bad news is that no matter what you do, there is a  
super-exponential complexity result on proof-length for Presburger  
Artihmetic. So maybe, just let it be, or use reflection, i.e. the  
reflexifity theorem as any proof of Presburger :)

Best,
Amine.

Quoting Tobias Nipkow <nipkow at in.tum.de>:

> All of the lemmas involved are either arihmetic or logical inference  
> rules and make sense. Presburger is a generic and complex decision  
> procedure. I am not surprised and would not want to optimize  
> presburger to use fewer lemmas.
>
> Tobias
>
> Am 28/06/2011 00:08, schrieb Jasmin Blanchette:
>> Hi all,
>>
>> Quick question: Josef Urban noticed that the proof terms for some  
>> lemmas proved directly by "presburger" can refer to lots of other  
>> lemmas; for example, the proof of "Parity.even_mult_two_ex"  
>> directly refers to 206 lemmas.
>>
>> ML {* Thm.proof_body_of @{thm Parity.even_mult_two_ex} *}
>>
>> (I've attached the list.) Is that normal? Does this have anything  
>> to do with "presburger"?
>>
>> Jasmin
>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>