http://blog.gmane.org/gmane.comp.mathematics.mizar hourly 1 1901-01-01T00:00+00:00 http://gmane.org/img/gmane-25t.png http://gmane.org http://comments.gmane.org/gmane.comp.mathematics.mizar/1396 <pre>Hi, at http://mws.cs.ru.nl/~mptp/7.13.01_4.181.1147/MPTP2/00mmldupl.html is a list of 332 duplications in MML 7.13.01_4.181.1147 . Josef </pre> Josef Urban 2012-05-20T06:46:00 http://comments.gmane.org/gmane.comp.mathematics.mizar/1395 <pre>******************************************************************************** CALL FOR PARTICIPATION AT ESSLLI 2012 Meeting: 24th European Summer School in Logic, Language and Information (ESSLLI) Date: 06-Aug-2012 - 17-Aug-2012 Location: Opole, Poland Meeting URL: http://www.esslli2012.pl Early registration deadline: 15-06-2012 ******************************************************************************** **Meeting Description** For the past 24 years, the European Summer School in Logic, Language and Information (ESSLLI) has been organized every year by the Association for Logic, Language and Information (FoLLI) in different sites around Europe. The main focus of ESSLLI is on the interface between linguistics, logic and computation. ESSLLI offers foundational, introductory and advanced courses, as well as workshops, covering a wide variety of topics within the three areas of interest: Language and Computation, Language and Logic, and Logic and Computation. Previous summer schools have been highly su</pre> A. Herzig 2012-05-09T15:30:00 http://comments.gmane.org/gmane.comp.mathematics.mizar/1392 <pre>There is known problem: which one to use? The denotation is the same, however technically the type 'real number' is more general than 'Element of REAL' Therefore one likes to have theorems about real numbers and one likes to prove theorems about elements of reals. The same goes for other kinds of numbers. However short notation (expandable type) is used as a rule for 'number' with an adjective: ORDINAL1: mode Nat is natural number; INT_1: mode Integer is integer number; RAT_1: mode Rational is rational number; CFUNCT_1: mode Complex is complex number; not so in the case of 'Real': REAL_1: mode Real is Element of REAL; If there are some arguments for both types, it is unacceptable that the user must look to the abstracts to check which type had been used in the theorem to which he wants to refer to. And if we have to choose, 'real number' is preferable. Changing the definition of the mode 'Real' causes too many errors, co some preparatory work is necessary. In the new version many</pre> trybulec< at >math.uwb.edu.pl 2012-05-11T09:28:25 http://comments.gmane.org/gmane.comp.mathematics.mizar/1389 <pre>[Apologies if you receive multiple copies] *** Post-proceedings will appear in EPTCS *** ------------------------------------------------ --- Final Call for Papers --- 10th International Workshop on User Interfaces for Theorem Provers (UITP 2012) 11.07.2012, Bremen, Germany, Part of CICM 2012 http://www.informatik.uni-bremen.de/uitp12/ While interactive theorem provers have found many new application areas in the last years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain relatively basic and under-designed. More and more, this is becoming an obstacle for the wider adoption of theorem proving technologies outside the academic community. The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with interactive proof systems, be it theorem provers, formal method tools, and other tools manipulating and presenting mathematical f</pre> Cezary Kaliszyk 2012-04-25T14:01:14 http://comments.gmane.org/gmane.comp.mathematics.mizar/1387 <pre>---------------------------------------------------------------------- 2nd CALL FOR PAPERS ---------------------------------------------------------------------- THedu'12 TP components for educational software 11 July 2012 http://www.uc.pt/en/congressos/thedu/thedu12 Workshop at CICM 2012 Conferences on Intelligent Computer Mathematics 9-14 July 2012 Jacobs University, Bremen, Germany http://www.informatik.uni-bremen.de/cicm2012/cicm.php ---------------------------------------------------------------------- THedu'12 Scope -------------- This workshop intends to gather the research communities for computer Theorem proving (TP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS). The</pre> Makarius 2012-04-16T18:25:30 http://comments.gmane.org/gmane.comp.mathematics.mizar/1382 <pre>[apologies for multiple copies] MIR 2012 Workshop (Mathematics Information Retrieval) July 14. 2011 at CICM 2012, Bremen Germany http://cicm2012.cicm-conference.org/cicm.php?event=mir The MIR Workshop brings together researchers working on information retrieval for mathematical document collections for discussions and friendly systems competition. Workshop format: =========== The MIR Workshop will consist of a traditional-style scientific program with presentations of submitted papers in the half-day Math IR Symposium together with the Math IR happening, where workshop participants competitively or jointly solve a set of Math IR challenges and submit their solutions to a panel of mathematician judges. Important dates: - Symposium: Paper Submission: May 20. 2012 Notification: May 28. 2012 Final Versions:June 15. 2012 - Happening: Dataset available: now System Registration: May 20. 2012 Organizers: Micha</pre> m.kohlhase< at >jacobs-university.de 2012-03-29T16:34:10 http://comments.gmane.org/gmane.comp.mathematics.mizar/1381 <pre>Some new developments by the Mizar team for parsing and normalizing Mizar texts are now available through an HTTP interface at http://mizar.cs.ualberta.ca/parsing/ With one of the transformations ("Weakly Strict Mizar") one can in principle write a simple parser for Mizar using, e.g., bison. (Since the set of arbitrary Mizar texts is syntactically rather complex, this is an important normalization step.) If one prefers a complete XML parse tree, that is also available. From the new Mizar parsing site one can download a Perl script, mizparse.pl, for parsing and transforming Mizar texts in these new ways (the script simply prepares an HTTP message and sends it to the HTTP service there). Get it from: http://mizar.cs.ualberta.ca/parsing/mizparse.pl Other allied utilities (e.g., pretty-printing) are under development. If you have any questions, comments, or feature requests, I'm happy to entertain them. Enjoy, Jesse </pre> Jesse Alama 2012-03-20T10:30:07 http://comments.gmane.org/gmane.comp.mathematics.mizar/1380 <pre>Hi, the HTML/ATP services now use tooltips (balloon help as in Emacs) for showing thesis, the meaning of the used library references, the meaning of property/correctness formulas, proofs, and ATP explanations. Clicking should work as before (it seems good to combine both these methods when reading proofs). A normal example is http://mizar.cs.ualberta.ca/~mptp/7.13.01_4.181.1147/html/card_1.html . An example with tooltips over the "by/from" keywords showing also ATP explanations is http://mizar.cs.ualberta.ca/~mptp/cgi-bin/MizAR.cgi?ProblemSource=URL&amp;FormulaURL=http://mizar.cs.ualberta.ca/~mptp/mml4.181.1147/mml/card_1.miz&amp;MMLVersion=4.181.1147&amp;Name=Tst1&amp;GenATP=1&amp;HTMLize=1 (or use the interface at http://mizar.cs.ualberta.ca/~mptp/MizAR.html, or the html-ization from Emacs). I have only tested with Firefox and Chrome so far, no idea what the code does in Explorer. Best, Josef </pre> Josef Urban 2012-03-20T02:20:08 http://comments.gmane.org/gmane.comp.mathematics.mizar/1375 <pre>Please promote Lm9 of XCMPLX_1 (MML 4.181.1147) for a, b being complex number st a &lt;&gt; 0 holds a / (a / b) = b to a proper theorem. It is quite silly to repeat the proof of this fact in an article. Imagine if a mathematician stated and proved this lemma in a paper on advanced complex analysis, with an apology: "The author of this useful lemma forbade me from citing it, so I have to reinvent this little wheel. Let a and b be complex numbers, and assume that a is nonzero. ..." In fact, why not promote *all* the lemmas of XCMPLX_1 to proper theorems? In this kind of article (part of the Encyclopedia), its many lemmas might be useful in many contexts. No private lemmas, please! More generally, I am not convinced of the value of unexported theorems. Neither an author nor the MML Library Committee knows just when a lemma might be useful for other people in contexts they don't currently work with. Sure, in the course of writing an article (or maintaining it in light of other changes to the library), i</pre> Jesse Alama 2012-03-16T12:39:22 http://comments.gmane.org/gmane.comp.mathematics.mizar/1373 <pre>Here are frequencies (&gt;1) of sentence starters in some 40k mathematical sentences. It seems that Mizar got the keywords quite right (modulo "suppose" vs. "assume"). Josef 9425 Let 5387 Then 2994 So 2338 The 2127 From 1936 Thus 1803 We 1586 Hence 1354 By 1267 This 1048 Now 926 Suppose 904 That 902 If 887 Therefore 886 But 808 As 696 Since 678 It 533 For 396 In 298 Also 276 Similarly 272 Consider 238 First 221 Note 210 Follows 158 There 147 Because 146 However 129 Finally 126 To 122 Every 115 Next 88 These 85 When 76 Take 76 Proof 71 Using 71 All 69 Define 69 Assume 63 Clearly 62 Given 61 Otherwise 60 Again 59 On 57 Furthermore 57 Each 53 Taking 52 Alternatively 48 Conversely 47 Some 47 An 45 Join 44 Any 43 And 42 Its 36 Putting 35 Moreover 33 Checking </pre> Josef Urban 2012-03-15T20:47:37 http://comments.gmane.org/gmane.comp.mathematics.mizar/1350 <pre>Let me make one thing clear: we do not propose to chang the foundations of MML. The chang eis rather related to type handling. The (quite old/brand new) TARSKI:1 will be for x being element holds x is set It now obvious that 2 is a set, I mean 2 is set; is accepted without any references. In new approach it will need justification: 2 is set by TARSKI:1; I used many times (and it must be revised) 1-sorted(#1, ... #) for 1-element 1-sorted. I even wanted to do a revision :-). With new approach one must write 1-sorted(#{0}, ...#) that means the same and it less tricky. Regards, Andrzej </pre> trybulec< at >math.uwb.edu.pl 2012-03-12T11:59:27 http://comments.gmane.org/gmane.comp.mathematics.mizar/1349 <pre> ----- Przekazana wiadomość od arturk&lt; at &gt;math.uwb.edu.pl ----- Data: Mon, 12 Mar 2012 11:41:44 +0100 (CET) Od: Artur Kornilowicz &lt;arturk&lt; at &gt;math.uwb.edu.pl&gt; Odpowiedz-Do:developer-forum&lt; at &gt;mizar.uwb.edu.pl Temat: [dev-forum] Re: Urelements? Do: Developer-Forum &lt;developer-forum&lt; at &gt;mizar.uwb.edu.pl&gt; Just to present some results. The columns are: article time_without_expansions time_with_exp difference_in_seconds They are sorted wrt 4th column. nat_4 1:18 27:17 1559 menelaus 0:36 10:48 612 sf_mastr 0:49 8:44 475 abcmiz_1 1:47 7:20 333 jordan9 1:07 6:29 322 jordan13 1:05 6:15 310 euclid_6 0:56 6:01 305 enumset1 0:01 4:39 278 euclid_3 0:14 4:45 271 fomodel3 2:31 6:42 251 convex4 0:28 4:38 250 jordan 3:29 7:32 243 matrix_9 1:28 5:26 238 nat_1 0:02 3:54 232 topgen_5 1:11 4:17 186 scpqsort 3:59 7:05 186 borsuk_5 0:05 3:09 184 scmbsort 1:50 4:50 180 borsuk_7 1:37 4:30 173 aofa_i00 1:36 4:28 172 circuit1 0:35 3:19 164 jordan1h 0:56 3:22 146 fomodel2 1:25 3:38 133 matrix15 1:23 3:30 127 fomodel0 0:35 2:42 1</pre> trybulec< at >math.uwb.edu.pl 2012-03-12T11:48:34 http://comments.gmane.org/gmane.comp.mathematics.mizar/1345 <pre>Hi; I would like to start with Polish "Nie przesadzajmy, jak mawiał leniwy ogrodnik", I do not know how to translate it. I wonder what Google does with it. It seems that we exaggerated with the statement that everything is a set. Actually numbers and structures behave rather like urelements (I am aware that elements of structures are supposed to be urelements, not the structures themselves). In old Mizar the root type (and mode) was 'Any'. The type 'set' was a subtype of 'Any', the first axiom in TARSKI said that 'everything is a set'. One of the reason was that we planned to develop other repositories based e.g. on arithmetics, in which probably the first axiom would be 'everything is a natural number'. Then we decided that it is enough trouble with one MML, and keeping two different types with the same denotation is useless. Recently Artur started to experiment with definitional expansion of atomic sentences in the Inference Checker (CHECKER in the Mizar jargon) and the results are disgust</pre> trybulec< at >math.uwb.edu.pl 2012-03-11T17:21:52 http://comments.gmane.org/gmane.comp.mathematics.mizar/1343 <pre>Fixed variables are called sometimes local constants. Ground term is defined as 'a term that does not contain any variables at all' (Wikipedia). How to call a term that does not contain bound variables, but local constants are allowed? The same goes for closed terms and so on. BTW How to call variables that are not fixed. I tried to use 'quantified variables'. It is O.K. in the case of variables bound by quatifiers, not so is they are bound by operators. So I use 'bound variables'. On the other hand fixed variables are also bound, by proof constructors. Regards, Andrzej </pre> trybulec< at >math.uwb.edu.pl 2012-03-11T09:35:14 http://comments.gmane.org/gmane.comp.mathematics.mizar/1340 <pre>Hi, at https://raw.github.com/JUrban/mizarmode/master/lstlangmizar.sty is a basic LaTeX syntax highlighting mode for Mizar. Use it with Mizar code in LaTeX like this: \begin{lstlisting}[language=Mizar] ::$N Brouwer Fixed Point Theorem theorem Th14: for r being non negative (real number), o being Point of TOP-REAL 2, f being continuous Function of Tdisk(o,r), Tdisk(o,r) holds f has_a_fixpoint proof ... \end{lstlisting} Josef </pre> Josef Urban 2012-02-27T16:20:10 http://comments.gmane.org/gmane.comp.mathematics.mizar/1339 <pre>---------------------------------------------------------------------- CALL FOR PAPERS ---------------------------------------------------------------------- THedu'12 TP components for educational software 11 July 2012 http://www.uc.pt/en/congressos/thedu Workshop at CICM 2012 Conferences on Intelligent Computer Mathematics 9-14. July 2012 Jacobs University, Bremen, Germany http://www.informatik.uni-bremen.de/cicm2012/cicm.php ---------------------------------------------------------------------- THedu'12 Scope -------------- This workshop intends to gather the research communities for computer Theorem proving (TP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic Geometry Systems (</pre> Makarius 2012-02-27T13:20:31 http://comments.gmane.org/gmane.comp.mathematics.mizar/1338 <pre> ** Workshop on Automation in Proof Assistants 2012 ** a satellite workshop of ETAPS 2012 jointly organized with the Rich-Model Toolkit COST action Sat 31 March - Sun 1 April, Tallinn, Estonia http://pauillac.inria.fr/~herbelin/aipa2012 Regular registration fees end *** 26 February 2012 *** ** Invited speakers ** Jean-Christophe Filliâtre (U. Paris-Sud): Why3 Jasmin Blanchette (T.U. Munich): Sledgehammer, Quickcheck, and Nitpick Chad E. Brown (U. Saarland): Satallax ** Contributing a talk ** The workshop will be informal. In addition to invited talks, the workshop will be based on contributed talks and discussions. To contribute a talk, send a title and abstract to aipa2012(at)inria.fr. ** Program committee ** Keijo Heljanko (Aalto University, IC0901 chair) Hugo Herbelin (INRIA Paris-Rocquencourt, AIPA chair) Viktor Kuncak (EPFL, Lausanne) Adam Naumowicz (University of Białystok) Claudio Sacerdoti (University of Bologna) Makarius Wenzel (University Par</pre> Hugo Herbelin 2012-02-24T22:09:52 http://comments.gmane.org/gmane.comp.mathematics.mizar/1337 <pre> Dear All, together with the latest official version of the Mizar system (7.13.01, MML version 4.181.1147) the following new Mizar articles are available: 1133. ZMODUL01 $\mathbb Z$-modules by Yuichi Futa, Hiroyuki Okazaki and Yasunari Shidama Received September 5, 2011 1134. MORPH_01 Morphology for Image Processing, Part {I} by Hiroshi Yamazaki, Czes\l aw Byli\'nski and Katsumi Wasaki Received September 21, 2011 1135. NDIFF_4 The Differentiable Functions from $\mathbbR$ into ${\mathbbR}^n$ by Keiko Narita, Artur Korni\l owicz and Yasunari Shidama Received September 28, 2011 1136. MATRIX17 Some Basic Properties of Some Special Matrices, Part {III} by Xiquan Liang and Tao Wang Received October 23, 2011 1137. INTEGR19 Riemann Integral of Functions from $\mathbbbR$ into $n$-dimensional Real Normed Space by Keiichi Miyajima, Artur Korni{\l}owicz and Yasunari Shidama Received October 27, 2011 1138. EC_PF_2 </pre> Adam Grabowski 2012-02-22T08:13:21 http://comments.gmane.org/gmane.comp.mathematics.mizar/1336 <pre>---------- Forwarded message ---------- Date: Tue, 21 Feb 2012 21:47:05 +0100 (CET) From: Makarius &lt;makarius&lt; at &gt;sketis.net&gt; To: adamn&lt; at &gt;math.uwb.edu.pl Subject: CICM 2012 -- last call for papers I am not sure if the subsequent CFP made it on the list as intended. The abstract deadline has passed already yesterday, but there is about one more week left for the main submission deadline. Moreover, the PC chairs have agreed to be flexible to accomodate late submissions. Makarius ---------- Forwarded message ---------- Date: Fri, 17 Feb 2012 11:15:14 +0100 From: Johan Jeuring &lt;J.T.Jeuring&lt; at &gt;uu.nl&gt; To: om&lt; at &gt;openmath.org, om-announce&lt; at &gt;openmath.org, poplmark&lt; at &gt;lists.seas.upenn.edu, project-calculemus&lt; at &gt;lists.jacobs-university.de, project-latexml&lt; at &gt;lists.jacobs-university.de, projects-mkm-ig&lt; at &gt;jacobs-university.de, project-omdoc&lt; at &gt;lists.jacobs-university.de, proofpower&lt; at &gt;lemma-one.com, pvs&lt; at &gt;csl.sri.com Subject: [MKM-IG] Conference on Intelligent Computer Mathematics, last call for </pre> Adam Naumowicz 2012-02-22T05:34:46 http://comments.gmane.org/gmane.comp.mathematics.mizar/1334 <pre>UITP'12: First Call for Papers [Apologies if you receive multiple copies] ------------------------------------------ --- First Call for Papers --- 10th International Workshop on User Interfaces for Theorem Provers (UITP 2012) 11.07.2012, Bremen, Germany, Part of CICM 2012 http://www.informatik.uni-bremen.de/uitp12/ While interactive theorem provers have found many new application areas in the last years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain relatively basic and under-designed. More and more, this is becoming an obstacle for the wider adoption of theorem proving technologies outside the academic community. The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with interactive proof systems, be it theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas. For t</pre> Cezary Kaliszyk 2012-02-02T19:07:52 http://comments.gmane.org/gmane.comp.mathematics.mizar/1322 <pre> ** Workshop on Automation in Proof Assistants 2012 ** a satellite workshop of ETAPS 2012 jointly organized with the Rich-Model Toolkit COST action Sat 31 March - Sun 1 April, Tallinn, Estonia http://pauillac.inria.fr/~herbelin/aipa2012 Early registration before *** 29 January 2012 *** Though proof assistants such as Agda, Coq, Isabelle, Matita, Mizar, Twelf, but also ACL2, HOL-Light, HOL4, PVS and many others are characterized as interactive theorem provers, automation is largely present under different forms in them, and at the same time probably not as present as what one would like. The purpose of this workshop is to gather people working on all different aspects of automation relevant for interactive theorem proving, starting with the following topics: * decision procedures on specific domains * connecting interactive and automated theorem provers * combination of decision procedures * reflection techniques * unification techniques and heuristics * rewr</pre> Hugo Herbelin 2012-01-25T16:05:59 Search the mailing list at Gmane query http://search.gmane.org/?group=$group=gmane.comp.mathematics.mizar