Re: [isabelle] Proving lemmas containing a squareroot



2010/6/4 grechukbogdan <grechukbogdan at yandex.ru>:
> Hi
>
> The lemma "ALL a b. (4) / pl a > (4) / pl b" is not correct. Counterexample a=b
> May be, you wanted to say "EX a b. (4) / pl a > (4) / pl b"?
>

That's correct; sorry for the typo. Like wise for rt4 and it should
read "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" instead. So anyone
knows what theorems are needed for rt4 and why metis won't terminate?

Thanks
Michael

> Bogdan.
>
>
> 04.06.10, 08:15, "Michael Daniels" <dayzman at gmail.com>:
>
>> Hi
>>
>>  I'm hoping some of you could help me with the following lemma:
>>
>>  consts
>>  pl :: "real => real"
>>
>>  axioms
>>  gt: "EX x y. pl x > pl y"
>>
>>  lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
>>  using gt
>>  sledgehammer;
>>
>>  It seems like a rather simple lemma but sledgehammer (E, SPASS, and
>>  Vampire) can't seem to return the set of theorems for metis. Does
>>  anyone know how to prove it?
>>
>>  Moreover, if I simplify the lemma by removing the sqrt to:
>>
>>  lemma rt4: "ALL a b. (4) / pl a > (4) / pl b"
>>  using gt
>>  sledgehammer;
>>
>>  Vampire gives me a minimal set of 14 theorems for metis:
>>
>>  apply (metis comm_monoid_add.mult_commute comp_arith(112)
>>  divide_inverse eq_diff_eq' eq_number_of inverse_inverse_eq
>>  linorder_neqE_ordered_idom monoid_add_class.add_0_right
>>  mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
>>  rel_simps(38) rel_simps(46))
>>
>>  However, metis actually will not terminate. Assuming those 14 theorems
>>  are the required theorems, why is having sqrt so difficult for
>>  sledgehammer?
>>
>>  Thanks!
>>
>>  Michael
>>
>>
>>
>
> --
> Здесь спама нет http://mail.yandex.ru/nospam/sign
>





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