[Hol-info] SEFM 2019 - Call for Papers

Second Call for Papers SEFM 2019 17th International Conference on Software Engineering and Formal Methods Oslo, Norway, September 16-20, 2019 ht

[Hol-info] LSFA 2019 - Second Call for papers

SECOND CALL FOR PAPERS LSFA 2019 14th Workshop on Logical and Semantic Frameworks, with Applications 24-26 August 2019, Natal, Brazil https://sites.google.com/view/lsfa2019 Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provid

[Hol-info] Proving a negative statement

I want to prove ``a <> b`` for some a,b. After stripping I am asked to prove F. I was able to use the assumptions to prove ``F = T``. At this point I thought "asm_simp_tac bool_ss []" should finish the proof but it doesn't. So "pop_assum (fn th => rewrite_tac [th]" actually finished the work for me

Re: [Hol-info] Proving a negative statement

Yes. You could also simplify in the assumptions by using fs[] which should work. Michael From: Haitao Zhang Date: Wednesday, 13 March 2019 at 12:27 To: hol-info Subject: [Hol-info] Proving a negative statement I want to prove ``a <> b`` for some a,b. After stripping I am asked to prove F.