Re: [isabelle] Proving equivalence



Hi,

Thanks for pointing out the inconsistency. Just curious, how could you could spot the inconsistency? How could "(0::real) = 1" be derived from that axiom?

Thanks again

Steve

On Jan 25, 2011 6:11pm, Brian Huffman <brianh at cs.pdx.edu> wrote:
Hi Steve,



As Tjark pointed out recently, axioms are evil. It just so happens

that both of your example axiomatizations are inconsistent. As you can

see:



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!



- Brian



On Tue, Jan 25, 2011 at 9:18 AM, Tjark Weber webertj at in.tum.de> wrote:

> Steve,

>

> 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

> fails.

>

> Kind regards,

> Tjark

>

>

>






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