[Hol-info] KR18 - Call for Tutorial and Workshop Proposals

2017-10-23 Thread Marcello Balduccini
[Apologies if you receive multiple copies of this email. Please distribute to interested parties.] KR18 - Call for Tutorial and Workshop Proposals ** Apologies if you receive multiple copies of this call ** ** Please distribute to interested parties ** C

[Hol-info] CfP: Models for Formal Analysis of Real Systems (MARS 2018)

2017-10-23 Thread Rob van Glabbeek and Wendelin Serwe
Call for Papers Workshop on Models for Formal Analysis of Real Systems (MARS 2018) April 21, 2018 Affiliated With ETAPS 2018 T

[Hol-info] CiE 2018: Preliminary announcement

2017-10-23 Thread Florin Manea
Appologies for multiple postings. = PRELIMINARY ANNOUNCEMENT: = CiE 2018: Sailing Routes in the World of Computation Kiel, Germany July 30 - August 3, 2018 http://cie2018.uni-kiel.de IMPORTANT DATES (tentative): Dea

[Hol-info] CAV 2018: Call for papers

2017-10-23 Thread no-reply
CAV 2018: The 30th International Conference on Computer Aided Verification July 14-17 2018, Oxford, UK, Part of the Federated Logic Conference, FLoC 2018 http://cavconference.org/2018/ http://floc2018.org Important dates: Paper submission deadline: January 31, 2018 (firm) Rebuttal period: Marc

Re: [Hol-info] Small question about sqrt

2017-10-23 Thread Liu Gengyang
It seems doesn't work. Could you please explain it in detail? -Original Messages- From:"Ramana Kumar" Sent Time:2017-10-23 05:38:07 (Monday) To: "Liu Gengyang" <2015200...@mail.buct.edu.cn> Cc: hol4_QA Subject: Re: [Hol-info] Small question about sqrt In your first goal, do either of t

Re: [Hol-info] Small question about sqrt

2017-10-23 Thread Liu Gengyang
Thanks, I think that's the reason, too. -Original Messages- From:michael.norr...@data61.csiro.au Sent Time:2017-10-23 07:17:02 (Monday) To: hol-info@lists.sourceforge.net Cc: Subject: Re: [Hol-info] Small question about sqrt Square root is unspecified on numbers < 0, so you don’t know

Re: [Hol-info] On the order of "variable" substitutions in lists or recursive structures

2017-10-23 Thread Chun Tian
Hi Konrad, Thank you very much! I’m learning finite_mapTheory now. Regards, Chun > Il giorno 23 ott 2017, alle ore 20:42, Konrad Slind > ha scritto: > > Hi Chun Tian, > > There are all kinds of issues with substitutions and applying them to > term-like > structures. I would probably sta

Re: [Hol-info] On the order of "variable" substitutions in lists or recursive structures

2017-10-23 Thread Konrad Slind
Hi Chun Tian, There are all kinds of issues with substitutions and applying them to term-like structures. I would probably start by choosing finite maps (finite_mapTheory) as the representation for variable substitutions since they get rid of most if not all the issues with ordering of replaceme

[Hol-info] On the order of "variable" substitutions in lists or recursive structures

2017-10-23 Thread Chun Tian
Hi, Suppose I have a list (or recursive structure defined by Datatype) in which there’re some special elements marked as “variables”, e.g. ``var X``, ``var Y``, … and I have a substitution function which correctly replaces a variable into another closed term (i.e. term without variables), and

Re: [Hol-info] LRTC (Reflexive Transitive Closure with a List)

2017-10-23 Thread Chun Tian
Hi Michael, Thanks, I’ll see if I can directly use something from pathTheory. Regards, Chun > Il giorno 23 ott 2017, alle ore 02:23, michael.norr...@data61.csiro.au ha > scritto: > > I’m afraid I can’t now remember if someone has already pointed this out, but > I think you probably should us