Re: [isabelle] Proving equivalence
Thanks for pointing out the inconsistency. Just curious, how could you
could spot the inconsistency? How could "(0::real) = 1" be derived from
On Jan 25, 2011 6:11pm, Brian Huffman <brianh at cs.pdx.edu> wrote:
As Tjark pointed out recently, axioms are evil. It just so happens
that both of your example axiomatizations are inconsistent. As you can
lemma "(0::real) = 1"
using ax1 by metis
(The same proof works also for ax2.)
This might explain why metis can easily solve your lemma: because from
ax1 or ax2 metis can prove any equation between real numbers!
On Tue, Jan 25, 2011 at 9:18 AM, Tjark Weber webertj at in.tum.de> wrote:
> On Tue, 2011-01-25 at 16:51 +0000, Steve W wrote:
>> Auto can't find a proof. How come this is so difficult for auto? What
>> is the proper way to do this proof?
> both "by blast" and "by metis" succeed. I didn't investigate why auto
> Kind regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and