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 <[email protected]>:
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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
