Re: [Hol-info] A problem of derivation

Hi Thomas, Thanks for your detailed answers, now I know what is the problem. Thanks again! Liu -Original Messages- From:"Thomas Tuerk" Sent Time:2017-11-09 11:35:14 (Thursday) To: hol-info@lists.sourceforge.net, "Liu Gengyang" <2015200...@mail.buct.edu.cn>

Re: [Hol-info] A problem of derivation

Thank you very much,its works! -Original Messages- From:michael.norr...@data61.csiro.au Sent Time:2017-11-09 11:15:52 (Thursday) To: 2015200...@mail.buct.edu.cn Cc: Subject: Re: [Hol-info] A problem of derivation Use the theorem SQRT_POW_2. E.g.: Q.prove( `!a b c d.(sqrt(c pow

Re: [Hol-info] A problem of derivation

Hi Liu, rewriting applies the provided equations left to write.  So if if have (A = A') /\ (B = B') ==> (f A B) The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B') as context and adds the rewrite rules A -> A' B -> B' where "->" is an ad-hoc notation for "=" but only

[Hol-info] FW: A problem of derivation

From: "Norrish, Michael (Data61, Acton)" Date: Thursday, 9 November 2017 at 14:15 To: Liu Gengyang <2015200...@mail.buct.edu.cn> Subject: Re: [Hol-info] A problem of derivation Use the theorem SQRT_POW_2. E.g.: Q.prove( `!a b c d.(sqrt(c pow 2 + d pow 2)

[Hol-info] A problem of derivation

Hi, I want to prove the goal: !a b c d.(sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\ (sqrt(a pow 2 + b pow 2) pow 2 = a pow 2 + b pow 2) /\ sqrt(c pow 2 + d pow 2) pow 2 ≤ sqrt(a pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤ a pow 2 + b pow 2 In theory this goal can be proved by

[Hol-info] IJCAR 2018 - Call for Papers

CALL FOR PAPERS The 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Oxford, UK, July 14-17, 2018. http://www.ijcar2018.org Part of The Federated Logic Conference, FLoC 2018, Oxford, UK, July 6-19, 2018. http://www.floc2018.org

[Hol-info] TPNC 2017: call for posters

TPNC 2017: call for posters*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line* - The 6th International Conference on the Theory and Practice of Natural Computing (TPNC 2017) invites researchers to submit