You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(12) 
_{Sep}
(8) 
_{Oct}
(20) 
_{Nov}
(21) 
_{Dec}
(3) 

2004 
_{Jan}
(16) 
_{Feb}
(11) 
_{Mar}
(26) 
_{Apr}
(15) 
_{May}
(17) 
_{Jun}
(10) 
_{Jul}
(3) 
_{Aug}
(4) 
_{Sep}
(11) 
_{Oct}

_{Nov}
(11) 
_{Dec}
(8) 
2005 
_{Jan}
(16) 
_{Feb}
(18) 
_{Mar}
(22) 
_{Apr}
(23) 
_{May}
(17) 
_{Jun}
(22) 
_{Jul}
(10) 
_{Aug}
(9) 
_{Sep}
(13) 
_{Oct}
(26) 
_{Nov}
(26) 
_{Dec}
(31) 
2006 
_{Jan}
(29) 
_{Feb}
(35) 
_{Mar}
(20) 
_{Apr}
(23) 
_{May}
(35) 
_{Jun}
(17) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(18) 
_{Oct}
(12) 
_{Nov}
(16) 
_{Dec}
(27) 
2007 
_{Jan}
(27) 
_{Feb}
(22) 
_{Mar}
(15) 
_{Apr}
(38) 
_{May}
(26) 
_{Jun}
(24) 
_{Jul}
(8) 
_{Aug}
(20) 
_{Sep}
(21) 
_{Oct}
(23) 
_{Nov}
(20) 
_{Dec}
(24) 
2008 
_{Jan}
(16) 
_{Feb}
(19) 
_{Mar}
(24) 
_{Apr}
(54) 
_{May}
(24) 
_{Jun}
(21) 
_{Jul}
(20) 
_{Aug}
(12) 
_{Sep}
(19) 
_{Oct}
(28) 
_{Nov}
(26) 
_{Dec}
(34) 
2009 
_{Jan}
(22) 
_{Feb}
(15) 
_{Mar}
(20) 
_{Apr}
(33) 
_{May}
(27) 
_{Jun}
(30) 
_{Jul}
(23) 
_{Aug}
(13) 
_{Sep}
(21) 
_{Oct}
(19) 
_{Nov}
(29) 
_{Dec}
(22) 
2010 
_{Jan}
(36) 
_{Feb}
(30) 
_{Mar}
(58) 
_{Apr}
(38) 
_{May}
(34) 
_{Jun}
(35) 
_{Jul}
(22) 
_{Aug}
(8) 
_{Sep}
(40) 
_{Oct}
(27) 
_{Nov}
(29) 
_{Dec}
(23) 
2011 
_{Jan}
(31) 
_{Feb}
(39) 
_{Mar}
(30) 
_{Apr}
(49) 
_{May}
(38) 
_{Jun}
(27) 
_{Jul}
(11) 
_{Aug}
(13) 
_{Sep}
(20) 
_{Oct}
(28) 
_{Nov}
(23) 
_{Dec}
(18) 
2012 
_{Jan}
(36) 
_{Feb}
(39) 
_{Mar}
(61) 
_{Apr}
(71) 
_{May}
(188) 
_{Jun}
(117) 
_{Jul}
(132) 
_{Aug}
(153) 
_{Sep}
(32) 
_{Oct}
(44) 
_{Nov}
(64) 
_{Dec}
(56) 
2013 
_{Jan}
(85) 
_{Feb}
(36) 
_{Mar}
(44) 
_{Apr}
(130) 
_{May}
(47) 
_{Jun}
(33) 
_{Jul}
(34) 
_{Aug}
(25) 
_{Sep}
(20) 
_{Oct}
(49) 
_{Nov}
(20) 
_{Dec}
(39) 
2014 
_{Jan}
(38) 
_{Feb}
(61) 
_{Mar}
(83) 
_{Apr}
(56) 
_{May}
(42) 
_{Jun}
(37) 
_{Jul}
(24) 
_{Aug}
(16) 
_{Sep}
(28) 
_{Oct}
(16) 
_{Nov}

_{Dec}

S  M  T  W  T  F  S 

1

2

3

4
(1) 
5
(1) 
6
(2) 
7

8

9

10

11

12
(10) 
13
(2) 
14

15
(1) 
16

17
(1) 
18
(1) 
19
(7) 
20
(5) 
21
(2) 
22

23

24
(3) 
25

26
(2) 
27

28

29

30






From: John Harrison <John.H<arrison@cl...>  20070412 22:45:17

Hi Dan,  I'm doing some refinement proofs and am stuck with this goal:   `(!q. S q SUBSET S' q) ==> (!q. T' (S q) SUBSET T' (S' q))` As several people have pointed out, you need some restrictions on T' for this to be true. For example, if T' is the image operation based on another function, Behzad's suggestion would work. This is exactly why monotonicity of predicate transformers is such a big deal, and the theory is usually only wellbehaved in such cases. There's a bit of discussion of this in the HOL Light tutorial, starting in the middle of page 118 in the current version: http://www.cl.cam.ac.uk/~jrh13/hollight/tutorial_220.pdf The early part of Dijkstra's "A Discipline of Programming" is good on this topic. If a predicate transformer is nonmonotonic, it's hard to conceive of it as the weakest precondition of a program construct, even of a very exotic nondeterministic or miraculous kind. Compare page 114 of the tutorial where in a deep embedding you can easily show that any "wp" is monotonic for one notion of "program". John. 
From: John Harrison <John.H<arrison@cl...>  20070412 22:20:21

Hi Ewa,  let choice = new_definition `(!c1 c2. c1 \/ c2 <=> c1 [] c2)`;;   I get Exception: Noparse error message. This is a lexical issue rather than a logical problem. Certain characters are treated specially and not permitted to form part of multicharacter identifiers. The list of such characters is basically the "bracketlike" ones (see line 18 of the source file "parser.ml"). The justification for this is to avoid forcing the user to write spaces in various situations like "((x,y),z)" to avoid "((" parsing as a single token. You could change this by modifying the parser to liberalize the policy, but this may cause issues with other source files. I'd recommend that you just use a different symbol like "": # parse_as_infix("",(18,"right"));; val it : unit = () # let choice = new_definition `!c1 c2. c1  c2 <=> c1 \/ c2`;; val choice : thm =  !c1 c2. c1  c2 <=> c1 \/ c2 John. 
From: Behzad Akbarpour <Behzad.A<kbarpour@cl...>  20070412 21:02:34

Hi Dan; I think your goal can be proven by rewriting with the following theorem from HOL pred_set Theory: IMAGE_SUBSET:  !s t. s SUBSET t ==> !f. IMAGE f s SUBSET IMAGE f t Best Regards, Behzad On Apr 12 2007, Daniel Zingaro wrote: >Hi all, > >I'm doing some refinement proofs and am stuck with this goal: > >`(!q. S q SUBSET S' q) ==> (!q. T' (S q) SUBSET T' (S' q))` > >It seems true to me (if its not that also explains things =)), >however when I rewrite with the definitions of SUBSET and IN, nothing >obvious can solve it (MESON_TAC, SET_TAC, etc.). Does anyone have any >other ideas to try? > >Thanks, >Dan > > > >  > Take Surveys. Earn Cash. Influence the Future of IT Join > SourceForge.net's Techsay panel and you'll get the chance to share your > opinions on IT & business topics through brief surveysand earn cash > http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV > _______________________________________________ holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo 
From: Tjark Weber <tjark.weber@gm...>  20070412 20:53:32

Daniel, On Thursday 12 April 2007 22:35, Daniel Zingaro wrote: > I'm doing some refinement proofs and am stuck with this goal: > > `(!q. S q SUBSET S' q) ==> (!q. T' (S q) SUBSET T' (S' q))` > > It seems true to me (if its not that also explains things =)), I'm not really familiar with HOL Light's syntax, but if S, S', T' are just uninterpreted functions, your goal does not hold in general. To obtain a counterexample, consider any nonmonotonic operator for T', e.g. the complement operator. Tjark 
From: Lockwood Morris <lockwood@ec...>  20070412 20:50:37

I think it is not true. You may be subconsciously assuming that T' is a "pointwise" function, i.e. that T' satisfies, for all sets X, T' (X) = {t x  x IN X}, for some function t. If this is actually the case for your T', then the theorem expressing it should be your missing ingredient. But to see that your goal does not hold for settoset functions T' in general, try letting T' be set complement (with respect to whatever type S q and S' q are subsets of). Best wishes, Lockwood                        Lockwood Morris lockwood@... (315)4433046 Rm. 4125 CST Emeritus Professor Dept. of EECS Syracuse University Syracuse NY On Thu, 12 Apr 2007, Daniel Zingaro wrote: > Hi all, > > I'm doing some refinement proofs and am stuck with this goal: > > `(!q. S q SUBSET S' q) ==> (!q. T' (S q) SUBSET T' (S' q))` > > It seems true to me (if its not that also explains things =)), > however when I rewrite with the definitions of SUBSET and IN, nothing > obvious can solve it (MESON_TAC, SET_TAC, etc.). Does anyone have any > other ideas to try? > > Thanks, > Dan > > > >  > Take Surveys. Earn Cash. Influence the Future of IT > Join SourceForge.net's Techsay panel and you'll get the chance to share your > opinions on IT & business topics through brief surveysand earn cash > http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo > 
From: Daniel Zingaro <zingard@mc...>  20070412 20:35:27

Hi all, I'm doing some refinement proofs and am stuck with this goal: `(!q. S q SUBSET S' q) ==> (!q. T' (S q) SUBSET T' (S' q))` It seems true to me (if its not that also explains things =)), however when I rewrite with the definitions of SUBSET and IN, nothing obvious can solve it (MESON_TAC, SET_TAC, etc.). Does anyone have any other ideas to try? Thanks, Dan 
From: John Harrison <John.H<arrison@cl...>  20070412 03:40:32

Apologies if you've already got this, but I didn't see an announcement on the HOL or Isabelle lists, so it seemed worth repeating it. Note that one of the categories explicitly mentioned is "automated reasoning". John. KURT GOEDEL CENTENARY RESEARCH PRIZE FELLOWSHIPS The Kurt Goedel Society is proud to announce the commencement of the research fellowship prize program in honor of the celebration of Kurt Goedel's 100th birthday. The research fellowship prize program is sponsored by the John Templeton Foundation and will offer: * two Ph.D. (predoctoral) fellowships of $60,000 US per annum for two years * two postdoctoral fellowships of $80,000 US per annum for two years and * one senior fellowship of $120,000 US per annum for one year based on an international open competition, resulting in the publication of research papers in a special issue of a premier journal in mathematical logic. The following International Board of Jurors will be in charge of evaluating the applications: Peter ACZEL, University of Manchester (GB) Lev BEKLEMISHEV, Russian Academy of Sciences (RUS) John BURGESS, Princeton University (USA) Harvey FRIEDMAN, Ohio State University (USA) CHAIR John HARRISON, Intel Corporation (USA) Wilfried HODGES, Queen Mary University of London (GB) Simon KOCHEN, Princeton University (USA) Jan KRAJICEK, Academy of Sciences of the Czech Republic (CZ) Menachem MAGIDOR, Hebrew University (ISRAEL) Dave MARKER, University of Illinois at Chicago (USA) Michel PARIGOT, Universite Paris 7 (FRANCE) Pavel PUDLAK, Academy of Sciences of the Czech Republic (CZ) Hilary PUTNAM, Harvard University (USA) Jeff REMMEL,University of California at San Diego (USA) John STEEL, University of California at Berkley (USA) Frank STEPHAN, National University of Singapore (SINGAPORE) Albert VISSER, University of Utrecht (NL) Goal and Criteria of Merit The purpose of these fellowships is to support original research in, and areas surrounding, the foundations of mathematics. (See Scope below for more details.) These fellowships are intended to carry forward the legacy of Kurt Goedel, whose works exemplify deep insights and breakthrough discoveries in mathematical logic, with profound impact on the philosophy and foundations of mathematics. In pursuit of similar insights and discoveries, we adopt the following criteria of merit for evaluating Fellowship applications: 1. Intellectual merit, scientific rigor and originality of the submitted paper and work plan. The paper and research plans should combine visionary thinking with academic and scientific excellence. 2. Potential for significant contribution to basic fundamental issues of wide interest, and the likelihood for opening new, seminal lines of inquiry that bear on such issues. 3. Impact of the Fellowship on the project and likelihood that the Fellowship will make the proposed new lines of research possible. 4. The expectation that the proposed research will be successful. 5. Qualifications of the applicants will be evaluated on the basis of all available information including CV, research paper, research plans, research accomplishments, and letters of recommendation (recommendation letters are not required for senior applications). Scope Original fellowship proposals in the areas of * model theory * proof theory * recursion theory * set theory * foundations of mathematics * philosophy of mathematics * foundations of computer science (related to logic) * automated reasoning (related to logic) * complexity (related to logic) All fellowship proposals, regardless of subject area, will be judged according to * the relevance and resemblance of the research (finished and proposed) to the great insights and originality of Kurt Goedel * its general interest and clarity of motivation * its rigorous scientific quality and depth. Submission Instructions The three categories of fellowships are specified as follows: * Ph.D.(predoctoral): being in the stage before finishing the thesis (or equivalent achievements) * Postdoctoral: being in the stage within 10 years after finishing the thesis (or equivalent achievements) * Senior: being in a later stage The submission must consist of:  one document A in PDF format containing . the CV . the project description . the recommendation letters  one document B in PDF format containing the article  one text abstract relating to B Maximum allowed length of the abstract is 500 words. Document A containing the CV, the project description, and the recommendation letters must be prepared in the following way:   minimum font size: 10pt  paper size: A4  maximum length of the CV: 3 pages The CV must contain the list of all/most important publications. The CV must clearly state to which category the application belongs.  maximum length of project description: 4 pages Project description should clearly state where and at which institution the applicant intends to carry out the project.  minimum 2(two)/maximum 3 (three) 1page recommendation letters, in case of applications belonging to the categories Ph.D. (predoctoral) and postdoctoral fellowships. (The recommendation letters should be scanned and included into the PDF document) Document B containing the article to be published in Annals of Pure and Applied Logic must be prepared according to the guidelines of the Annals of Pure and Applied Logic. Please see http://www.elsevier.com/wps/find/journaldescription.cws_home/505603/authorinstructions for details. In a nutshell: Use LaTeX and elsart.cls. Maximum allowed length of the article is twentyfive (25) pages in the prescribed format. The submission must be in English. The Advisory Board and the Program Chair reserve the right . to consider only submissions with reasonable format . to reassign a submission to another category as applied for. The applicant will be informed about the reasons for such a decision. The submission software will be available online by the end of March. Timeline December 1, 2006.* Preannouncement June 30, 2007. Submissions deadline October 2007. Jury decision on the papers for publication (at most 20) December 15, 2007. Final versions due January 2008. Jury decision on winners due February 2008. Award Ceremony Mar.Sept.2008. Commencement of the Fellowships Web:http://kgs.logic.at/goedelfellowship Email contact: goedelfellowship@... * Date of the acceptance of Goedel's postdoctoral lecture qualification thesis in 1906. 
From: John Harrison <John.H<arrison@cl...>  20070412 02:36:04

Hi Ewa,  g `! p c q e invariant. p SUBSET invariant /\  (!X:S. correct (invariant INTER e INTER (\s. X = s)) c  (invariant INTER (\s. s <= X)))  ==> correct p (While e c) q`;;   I right away get error:  Exception: Failure "tryfind". This is a lousy error message, which I'll fix in the next release. It means that the system can't typecheck the term you entered by finding an overloaded interpretation of "<=" that would work on the type "S". You either need to fix your entire state space type as something like "num" or "int", or explicitly extract the field you want from a larger state space. Here is the former: g `! p c q e invariant. p SUBSET invariant /\ (!X:int. correct (invariant INTER e INTER (\s. X = s)) c (invariant INTER (\s. s <= X))) ==> correct p (While e c) q`;; John. 
From: Ewa Rom <ewuniar1@ho...>  20070412 02:17:26

Hi, =20 I'm trying to define an operator [] as a nondeterministic choice. I introduced the operator as:=20 parse_as_infix("[]",(18,"right"));; =20 I do not know however how to define it in HOL Light.=20 I would like it to act as an \/ (OR) operator, thus I try to define it as =20 let choice =3D new_definition `(!c1 c2. c1 \/ c2 <=3D> c1 [] c2)`;; =20 I get Exception: Noparse error message. =20 Thank you Ewa _________________________________________________________________ Discover the new Windows Vista http://search.msn.com/results.aspx?q=3Dwindows+vista&mkt=3DenUS&form=3DQBR= E= 
From: Ewa Rom <ewuniar1@ho...>  20070412 00:43:45

Hi, =20 I'm trying to prove that the variant is not increasing in a while loop. I created the following goal: =20 # g `! p c q e invariant. p SUBSET invariant /\ (!X:S. correct (invariant = INTER e INTER (\s. X =3D s)) c (invariant INTER (\s. s <=3D X))) =3D=3D> c= orrect p (While e c) q`;; =20 I right away get error: Exception: Failure "tryfind". =20 What does that mean? What am I doing wrong here? If I write: =20 # g `! p c q e invariant. p SUBSET invariant /\ (!X:S. correct (invariant = INTER e INTER (\s. X =3D s)) c (invariant INTER (\s. s < X))) =3D=3D> corr= ect p (While e c) q`;; =20 I get the same error message. =20 Thank you Ewa =20 _________________________________________________________________ Invite your mail contacts to join your friends list with Windows Live Space= s. It's easy! http://spaces.live.com/spacesapi.aspx?wx_action=3Dcreate&wx_url=3D/friends.= aspx&mkt=3Denus= 