gmane.comp.mathematics.mizar http://blog.gmane.org/gmane.comp.mathematics.mizar hourly 1 1901-01-01T00:00+00:00 Gmane http://gmane.org/img/gmane-25t.png http://gmane.org duplications in MML 7.13.01_4.181.1147 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 ESSLLI 2012 call for participation 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 successful, attracting up to 500 students from Europe and elsewhere. The school has developed into an important meeting place and forum for discussion for students and researchers interested in the interdisciplinary study of Logic, Language and Information. During two weeks, 49 courses and 6 workshops are offered to the attendants, each of 1.5 hours per day during a five days week, with up to seven parallel sessions. ESSLLI also includes a student session (papers and posters by students only, 1.5 hour per day during the two weeks). There will be three evening lectures by Mel Fitting, Jonathan Ginzburg and Adam Przepiorkowski. In 2012, ESSLLI will held in Opole, Poland and will be organized by the University of Opole, Poland. Chair of the program committee is Andreas Herzig, and chairs of the organizing committee are Urszula Wybraniec-Skardowska and Janusz Czelakowski. **Summer School Programme** http://www.esslli2012.pl/index.php?id=67 **Online Registration** http://www.esslli2012.pl/index.php?id=68 **Programme Committee** Chair: Andreas Herzig (Université de Toulouse and CNRS) Local co-chair: Anna Pietryga (University of Opole) Area specialists: Language and Computation: - Miriam Butt (Sprachwissenschaft, University of Konstanz) - Gosse Bouma (Groningen University) Language and Logic: - Regine Eckardt (Language and Literature, University of Göttingen) - Rick Nouwen (UiL-OTS, Utrecht University) Logic and Computation: - Natasha Alechina (CS, University of Nottingham) - Andreas Weiermann (Mathematics and Computation, Ghent University) **Organizing Committee** Chair: Urszula Wybraniec-Skardowska and Janusz Czelakowski (University of Opole) </pre> A. Herzig 2012-05-09T15:30:00 real number vs. Element of REAL 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 occurrences of 'Real' are changed to 'real number'. With more than 600 articles modified we decided to publish this new version of MML, even if the revolution is not completed. Sorry for the (even bigger) mess, we will correct it ASAP. Regards, Andrzej </pre> trybulec< at >math.uwb.edu.pl 2012-05-11T09:28:25 UITP'12: Final Call for Papers 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 formulas. For the forthcoming 10th UITP workshop, we invite contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. Topics covered include, but are not limited to: * Application-specific interaction mechanisms or designs for prover interfaces; * Experiments and evaluation of prover interfaces; * Languages and tools for authoring, exchanging and presenting proof; * Implementation techniques (e.g. web services, custom middleware, DSLs); * Integration of interfaces and tools to explore and construct proof; * Representation and manipulation of mathematical knowledge or objects; * Visualisation of mathematical objects and proof; * System descriptions. Submitted papers should describe previously unpublished work (completed or in progress), and not be longer than twelve pages. We encourage concise but relevant papers. Submissions should be in PDF format, and typeset with the EasyChair LaTeX document class (which can be downloaded from www.easychair.org), or in similar style. Submission are via EasyChair. All papers will be peer reviewed by members of the programme committee and selected by the organizers in accordance with the referee reports. Proceedings Accepted papers will appear in the workshop proceedings, which will be available in printed form at the workshop. After the workshop, revised papers can be submitted to a postproceedings, which will appear in EPTCS. Important Dates Submission deadline: 01.05.2012 Acceptance notification: 01.06.2012 Camera-ready copy: 15.06.2012 Program Committee: David Aspinall, University of Edinburgh, UK Serge Autexier, DFKI, Germany Christoph Benzmueller, Articulate Software, USA Herman Geuvers, Radboud University Nijmegen, the Netherlands Cezary Kaliszyk, University of Innsbruck, Austria, (PC co-chair) Christoph Lüth, DFKI, Germany (PC co-chair) Adam Naumowicz, University of Białystok, Poland Claudio Sacerdoti Coen, University of Bologna, Italy Geoff Sutcliffe, University of Miami, United States Enrico Tassi, INRIA, France Josef Urban, Radboud University Nijmegen, the Netherlands Makarius Wenzel, Université Paris-Sud 11, France </pre> Cezary Kaliszyk 2012-04-25T14:01:14 Thedu: 2nd Call for papers 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 workshop tries to combine and focus systems of these areas to enhance existing educational software as well as studying the design of the next generation of mechanised mathematics assistants (MMA). Elements for next-generation MMA's include: * Declarative Languages for Problem Solution: education in applied sciences and in engineering is mainly concerned with problems, which involve operations on elementary objects to be transformed to an object representing a problem solution. Preconditions and postconditions of these operations can be used to describe the possible steps in the problem space; thus, ATP-systems can be used to check if an operation sequence given by the user does actually present a problem solution. Such "Problem Solution Languages" encompass declarative proof languages like Isabelle/Isar or Coq's Mathematical Proof Language, but also more specialized forms such as, for example, geometric problem solution languages that express a proof argument in Euclidian Geometry or languages for graph theory. * Consistent Mathematical Content Representation: Libraries of existing ITP-Systems, in particular those following the LCF-prover paradigm, usually provide logically coherent and human readable knowledge. In the leading provers, mathematical knowledge is covered to an extent beyond most courses in applied sciences. However, the potential of this mechanised knowledge for education is clearly not yet recognised adequately: renewed pedagogy calls for inquiry-based learning from concrete to abstract --- and the knowledge's logical coherence supports such learning: for instance, the formula 2.pi depends on the definition of reals and of multiplication; close to these definitions are the laws like commutativity etc. However, the complexity of the knowledge's traceable interrelations poses a challenge to usability design. * User-Guidance in Stepwise Problem Solving: Such guidance is indispensable for independent learning, but costly to implement so far, because so many special cases need to be coded by hand. However, TP technology makes automated generation of user-guidance reachable: declarative languages as mentioned above, novel programming languages combining computation and deduction, methods for automated construction with ruler and compass from specifications, etc --- all these methods 'know how to solve a problem'; so, use the methods' knowledge to generate user-guidance mechanically, this is an appealing challenge for ATP and ITP, and probably for compiler construction! In principle, mathematical software can be conceived as models of mathematics: The challenge addressed by this workshop series is to provide appealing models for MMAs which are interactive and which explain themselves such that interested students can independently learn by inquiry and experimentation. Program Committee ----------------- Ralph-Johan Back, Abo Akademy University, Finland Francisco Botana, University of Vigo at Pontevedra, Spain Florian Haftman, Munich University of Technology, Germany Predrag Janicic, University of Belgrade, Serbia Cezary Kaliszyk, University of Tsukuba, Japan Julien Narboux, University of Strasbourg, France Filip Maric, University of Belgrade, Serbia Walther Neuper, Graz University of Technology, Austria Pedro Quaresma, University of Coimbra, Portugal Wolfgang Schreiner, Johannes Kepler University, Linz, Austria Laurent Théry, Sophia Antipolis, INRIA, France Makarius Wenzel, University Paris-Sud, France Burkhart Wolff, University Paris-Sud, France Important Dates (by easychair) --------------- * 01 May 2012 * Extended Abstracts/Demo proposals * 01 Jun 2012 * Author Notification * 15 Jun 2012 * Final Version * 11 Jul 2012 * Worshop Day * 31 Aug 2012 * Full papers (EPTCS post-proceedings) Submission ---------- We welcome submission of proposals to present a demo, as well as submissions of extended abstracts (5-8 pages max) presenting original unpublished work which is not been submitted for publication elsewhere. Selected extended abstracts will appear in CISUC Technical Report series (ISSN 0874-338X [1]). All accepted extended abstracts and system demos will be presented at the workshop, and the extended abstracts will be made available online. Extended abstracts and demo proposals should be submitted via THedu'12 easychair [2]. Extended abstracts should be 5-8 pages in length and are to be submitted in PDF format. They must conform to the EPTCS style guidelines [3]. At least one author of each accepted extended abstract/demo is expected to attend THedu'12 and presents her or his extended abstract/demo. The post-proceedings (full papers, 20 pages max) will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series [4]. --- [1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/ [2] http://www.easychair.org/conferences/?conf=thedu12 [3] http://http://style.eptcs.org/ [4] http://eptcs.org/</pre> Makarius 2012-04-16T18:25:30 CfP: Math Information Retrieval Worksohp 14. July 2012 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: Michael Kohlhase, Jacobs University (PC co-chair) Petr Sojka, Brno University (PC co-chair) Math IR Symposium at MIR 2012 ==================== http://cicm2012.cicm-conference.org/cicm.php?event=mir&amp;menu=symposium The Math IR Symposium is a traditional-style workshop with scientific contributions about mathematics information retrieval. Topics include but not limited to: - requirements for mathematics information retrieval: use cases and typical queries - formula search algorithms - semantically enhancing mathematical corpora for IR - extracting semantic relations from corpora. - evaluation of MIR (methods and test corpora) Math IR Happening at MIR 2012 ==================== http://cicm2012.cicm-conference.org/cicm.php?event=mir&amp;menu=happening A friendly competition for the systems presented at the workshop. Since math information retrieval is still quite young and developing, we will not make this an official competition, but a happening, where we get together and test our system on a common set of problems. We expect the happening to transcend the workshop proper. </pre> m.kohlhase< at >jacobs-university.de 2012-03-29T16:34:10 mizar parsing/text transformation service 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 tooltips 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 Lm9 of xcmplx_1 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), it might feel right to "hide" a lemma because it seems, at the time of writing, too specialized and therefore likely to have little reuse value to other authors. And for the purposes of a JFM version of an article, maybe it is reasonable to suppress some excessively specialized/customized lemmas. But with a growing MML, and greater reuse of more and more of its articles, I fail to see the value in hiding anything at all. Expose all theorems and let the community of users of the MML, not the author of a particular article, decide which lemmas are important. Even if one disagrees with this general view of unexported theorems, I still think that for articles like XCMPLX_1, which are supposed to lay out a large variety of useful theorems, I fail to see the value in keeping any theorem private (unexported). Jesse </pre> Jesse Alama 2012-03-16T12:39:22 vernacular 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 33 At 31 Here 30 Denote 29 What 26 They 26 See 24 Such 23 Both 20 Recall 20 Observe 18 He 17 Either 17 Draw 16 With 16 Substituting 16 Add 15 One 15 Construct 15 Combining 14 Multiplying 14 Further 14 Consequently 13 Two 13 Pick 13 Or 13 Notice 13 Likewise 13 Having 13 Choose 12 Trivially 12 Replace 12 Of 12 Although 11 Not 11 More 11 Compare 10 While 10 Which 10 Letting 10 Dividing 10 Call 10 Applying 10 After 9 Without 9 Substitute 9 Plugging 8 Subtract 8 Proceed 8 Our 8 Immediate 8 Expanding 8 Equivalently 8 Apply 8 According 7 Setting 7 Set 7 Select 7 Second 7 Repeat 7 Put 7 Fix 7 Eventually 6 Unless 6 Subtracting 6 Subsequently 6 Specifically 6 Once 6 Neither 6 Multiplication 6 Lastly 6 Differentiating 6 About 5 Writing 5 Write 5 Whether 5 Where 5 Whatever 5 Summing 5 Statement 5 Others 5 Is 5 Instead 5 Informally 5 File 5 Equality 5 Begin 5 Assuming 5 Another 5 Adding 4 Together 4 Throughout 4 Through 4 Their 4 Say 4 Other 4 Just 4 Evaluating 4 Elements 4 Base 3 You 3 Use 3 Uniqueness 3 Under 3 Sometimes 3 Replacing 3 Repeating 3 Rearranging 3 Place 3 Obviously 3 Noting 3 None 3 No 3 Make 3 Into 3 Indeed 3 Exactly 3 Even 3 Equally 3 Eliminating 3 Demonstrating 3 Continuity 3 Claim 3 Cases 3 Associativity 3 Arranging 2 Yeh 2 Waring 2 Upon 2 Trivial 2 Stated 2 Start 2 Squaring 2 Similar 2 Self 2 Reverse 2 Representing 2 Remove 2 Recalling 2 Real 2 Proving 2 Proved 2 Primes 2 Peirce 2 Output 2 Namely 2 Map 2 List 2 Joining 2 Interchanging 2 Integrating 2 Input 2 Induction 2 Identifying 2 How 2 Futhermore 2 Evidently 2 Euler 2 Doing 2 Directly 2 Differentiate 2 Defining 2 Continuing 2 Continue 2 Computing 2 Composing 2 Comparing 2 Choosing 2 Changing 2 Certainly 2 Case 2 Cancelling 2 Buchberger 2 Auxiliary 2 Assign 2 Apart 2 Additionally 2 Addition </pre> Josef Urban 2012-03-15T20:47:37 Urelements? 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 Fwd: [dev-forum] Re: Urelements? 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 127 cqc_the1 0:05 2:01 116 gfacirc1 1:08 3:03 115 abcmiz_a 0:29 2:22 113 jgraph_1 0:60 2:50 110 calcul_1 0:22 2:04 102 matrix13 1:47 3:15 88 scmfsa_i 0:02 1:29 87 goboard9 0:52 2:16 84 scmpds_4 0:13 1:34 81 uniroots 1:26 2:46 80 jgraph_5 1:10 2:29 79 anproj_2 0:06 1:25 79 graph_2 1:22 2:36 74 jgraph_6 2:09 3:22 73 jgraph_3 1:18 2:31 73 group_10 0:27 1:39 72 chord 1:19 2:31 72 matrtop1 1:02 2:12 70 zfmodel2 0:11 1:19 68 scmfsa6a 0:12 1:20 68 convex1 0:09 1:13 64 scmring3 0:19 1:21 62 jordan12 0:19 1:20 61 pre_poly 0:35 1:33 58 facirc_1 0:50 1:45 55 fomodel4 3:01 3:54 53 facirc_2 0:40 1:32 52 goboard5 0:15 1:06 51 jordan2c 2:17 3:07 50 sin_cos 0:49 1:37 48 amistd_5 0:28 1:16 48 pdiff_7 1:25 2:11 46 neckla_3 0:35 1:21 46 scmfsa_2 1:27 2:12 45 toprealb 1:15 1:59 44 toprealc 0:59 1:42 43 matrix11 1:41 2:24 43 hermitan 0:25 1:08 43 modal_1 0:22 1:03 41 matrixj2 1:50 2:30 40 exchsort 0:24 1:04 40 cohsp_1 0:35 1:15 40 topalg_5 1:09 1:48 39 scm_inst 0:05 0:44 39 sprect_1 0:40 1:18 38 seq_4 0:47 1:25 38 scm_comp 0:10 0:48 38 euclid_7 2:04 2:42 38 scm_halt 0:57 1:34 37 lpspace2 1:14 1:51 37 jordan19 1:38 2:15 37 fscirc_2 0:30 1:07 37 topalg_6 1:22 1:58 36 sprect_2 1:07 1:43 36 rlvect_2 0:22 0:57 35 necklace 0:08 0:43 35 moebius1 0:31 1:04 33 jordan7 0:38 1:11 33 int_4 0:35 1:08 33 group_9 4:28 5:01 33 matrtop2 0:54 1:26 32 jordan1g 1:15 1:47 32 diff_4 0:43 1:15 32 rlaffin3 0:58 1:29 31 msualg_9 0:26 0:57 31 jordan15 1:36 2:07 31 descip_1 6:23 6:54 31 mesfunc5 1:16 1:46 30 funct_7 0:16 0:46 30 catalan2 0:53 1:23 30 graph_3 1:50 2:18 28 revrot_1 0:20 0:47 27 holder_1 0:17 0:44 27 memstr_0 0:23 0:49 26 isocat_2 0:21 0:47 26 circuit2 0:38 1:04 26 stacks_1 0:14 0:39 25 finseq_3 0:19 0:44 25 numeral1 0:41 1:05 24 modelc_3 1:13 1:37 24 comput_1 1:13 1:37 24 compos_1 0:40 1:04 24 yellow11 0:10 0:33 23 sprect_3 0:42 1:05 23 gobrd11 0:33 0:56 23 fsm_1 0:50 1:13 23 circcmb3 0:32 0:55 23 cfdiff_1 0:18 0:41 23 brouwer 0:44 1:07 23 yellow18 0:15 0:37 22 jordan1j 0:58 1:20 22 card_fin 0:33 0:55 22 ami_6 0:16 0:38 22 integr11 0:34 0:55 21 amistd_1 0:28 0:49 21 afinsq_1 0:54 1:15 21 polynom3 0:36 0:56 20 pnproc_1 0:24 0:44 20 lattice5 0:32 0:52 20 goboard6 0:43 1:03 20 rlaffin1 0:33 0:52 19 quaterni 1:07 1:26 19 polyform 0:27 0:46 19 integra1 0:58 1:17 19 integr12 0:50 1:09 19 endalg 0:04 0:23 19 stirl2_1 0:47 1:05 18 rlaffin2 0:56 1:14 18 polynom5 0:49 1:07 18 mesfun7c 0:22 0:40 18 matrix14 0:19 0:37 18 goboard2 0:38 0:56 18 sin_cos2 0:22 0:39 17 pua2mss1 0:23 0:40 17 borsuk_6 0:42 0:59 17 uproots 1:02 1:18 16 mfold_2 0:48 1:04 16 jordan5b 0:25 0:41 16 afinsq_2 0:32 0:48 16 simplex1 0:43 0:58 15 rmod_4 0:08 0:23 15 limfunc1 0:25 0:40 15 jgraph_2 0:41 0:56 15 fdiff_3 0:45 0:60 15 algspec1 0:07 0:22 15 topalg_1 0:21 0:35 14 pscomp_1 0:45 0:59 14 polynom1 0:23 0:37 14 msualg_6 0:20 0:34 14 jordan23 0:21 0:35 14 fdiff_2 0:38 0:52 14 altcat_4 0:10 0:24 14 zf_lang1 0:12 0:25 13 waybel34 0:19 0:32 13 waybel29 0:27 0:40 13 waybel26 0:25 0:38 13 vectsp_6 0:08 0:21 13 trees_3 0:09 0:22 13 sin_cos3 0:09 0:22 13 scmfsa_4 0:13 0:26 13 dtconstr 0:19 0:32 13 bcialg_6 0:17 0:30 13 yellow20 0:09 0:21 12 vectsp10 0:12 0:24 12 topreal6 0:37 0:49 12 topreal1 0:21 0:33 12 robbins4 0:15 0:27 12 polyeq_5 2:37 2:49 12 oppcat_1 0:09 0:21 12 matrixj1 0:51 1:03 12 goboard1 0:28 0:40 12 finseq_4 0:09 0:21 12 complex2 0:19 0:31 12 circcomb 0:18 0:30 12 scmfsa_m 0:23 0:34 11 scmfsa10 0:22 0:33 11 rfunct_3 0:22 0:33 11 rcomp_3 0:28 0:39 11 pdiff_9 1:05 1:16 11 osafree 0:40 0:51 11 fib_num2 0:19 0:30 11 waybel27 0:21 0:31 10 topreal4 0:12 0:22 10 sppol_2 0:28 0:38 10 rvsum_2 0:08 0:18 10 rearran1 0:23 0:33 10 qc_lang2 0:03 0:13 10 prelamb 0:12 0:22 10 polynom6 0:16 0:26 10 ndiff_1 0:22 0:32 10 hurwitz 0:42 0:52 10 hilbert3 0:10 0:20 10 helly 0:19 0:29 10 fcont_1 0:22 0:32 10 csspace4 0:30 0:40 10 card_4 0:06 0:16 10 vectmetr 0:20 0:29 9 topreal9 0:21 0:30 9 topdim_2 0:28 0:37 9 tmap_1 0:10 0:19 9 scmyciel 0:20 0:29 9 rsspace4 0:24 0:33 9 pdiff_4 0:28 0:37 9 pcs_0 0:08 0:17 9 nat_3 0:22 0:31 9 mesfunc4 0:18 0:27 9 matrtop3 1:47 1:56 9 lattice8 0:15 0:24 9 kolmog01 0:19 0:28 9 integr16 0:12 0:21 9 ideal_1 0:40 0:49 9 hfdiff_1 0:26 0:35 9 gcd_1 0:08 0:17 9 finseq_1 0:12 0:21 9 cqc_sim1 0:22 0:31 9 compos_0 0:14 0:23 9 catalg_1 0:17 0:26 9 zmodul01 0:18 0:26 8 weierstr 0:07 0:15 8 topreal3 0:15 0:23 8 sin_cos6 0:25 0:33 8 pralg_3 0:11 0:19 8 pencil_3 0:13 0:21 8 pdiff_5 0:21 0:29 8 nagata_2 0:37 0:45 8 monoid_1 0:15 0:23 8 matrlin2 0:27 0:35 8 lopban_6 0:09 0:17 8 index_1 0:10 0:18 8 gobrd12 0:47 0:55 8 goboard3 0:20 0:28 8 fvaluat1 0:15 0:23 8 fomodel1 0:29 0:37 8 fdiff_11 0:31 0:39 8 fdiff_1 0:21 0:29 8 circtrm1 0:17 0:25 8 cfdiff_2 0:32 0:40 8 cat_5 0:12 0:20 8 card_2 0:06 0:14 8 sin_cos4 0:04 0:11 7 rfinseq 0:11 0:18 7 random_1 0:24 0:31 7 ordinal6 0:10 0:17 7 msalimit 0:09 0:16 7 mesfunc3 0:26 0:33 7 mazurulm 0:13 0:20 7 jordan_a 0:19 0:26 7 jordan6 0:22 0:29 7 jordan1a 0:25 0:32 7 isocat_1 0:05 0:12 7 integr13 0:17 0:24 7 group_7 0:11 0:18 7 glib_005 1:09 1:16 7 funct_9 0:12 0:19 7 extpro_1 0:08 0:15 7 euclid_9 0:21 0:28 7 dilworth 0:17 0:24 7 closure1 0:06 0:13 7 bilinear 0:13 0:20 7 altcat_2 0:10 0:17 7 abcmiz_0 0:15 0:22 7 zfmodel1 0:09 0:15 6 waybel18 0:12 0:18 6 valued_2 0:35 0:41 6 sublemma 0:44 0:50 6 scmpds_7 1:16 1:22 6 scmfsa7b 0:31 0:37 6 rlvect_4 0:03 0:09 6 quofield 0:10 0:16 6 pralg_1 0:09 0:15 6 ntalgo_1 4:26 4:32 6 ndiff_3 0:15 0:21 6 nattra_1 0:08 0:14 6 mssublat 0:11 0:17 6 matrix10 0:14 0:20 6 jordan5a 0:21 0:27 6 jgraph_8 0:24 0:30 6 integr15 0:25 0:31 6 hahnban 0:11 0:17 6 gobrd14 0:18 0:24 6 filter_1 0:17 0:23 6 euler_1 0:06 0:12 6 equation 0:15 0:21 6 combgras 0:22 0:28 6 cc0sp2 0:39 0:45 6 amistd_2 0:15 0:21 6 waybel25 0:20 0:25 5 trees_2 0:10 0:15 5 topreal2 0:35 0:40 5 topgen_3 0:11 0:16 5 tietze 0:20 0:25 5 series_2 0:33 0:38 5 rusub_3 0:11 0:16 5 rfunct_1 0:09 0:14 5 qc_lang1 0:08 0:13 5 osalg_4 0:14 0:19 5 newton 0:12 0:17 5 msinst_1 0:12 0:17 5 msafree3 0:14 0:19 5 monoid_0 0:13 0:18 5 modelc_2 0:44 0:49 5 measure7 0:10 0:15 5 matrix_7 1:09 1:14 5 lfuzzy_1 0:09 0:14 5 jordan5c 0:14 0:19 5 jordan21 0:16 0:21 5 jordan11 0:21 0:26 5 integr19 0:55 1:00 5 group_4 0:10 0:15 5 groeb_1 1:01 1:06 5 glib_003 0:38 0:43 5 functor0 0:33 0:38 5 extens_1 0:06 0:11 5 dist_1 0:06 0:11 5 clvect_1 0:09 0:14 5 chain_1 0:34 0:39 5 cc0sp1 0:33 0:38 5 cardfin2 0:13 0:18 5 bvfunc_1 0:30 0:35 5 bspace 0:06 0:11 5 borsuk_2 0:11 0:16 5 zf_fund1 0:06 0:10 4 yellow_9 0:09 0:13 4 yellow16 0:07 0:11 4 yellow15 0:07 0:11 4 waybel_6 0:11 0:15 4 triang_1 0:13 0:17 4 trees_9 0:10 0:14 4 topalg_4 0:11 0:15 4 topalg_3 0:11 0:15 4 seq_2 0:10 0:14 4 scmpds_9 0:08 0:12 4 reloc 0:17 0:21 4 ranknull 0:09 0:13 4 prob_3 0:11 0:15 4 pre_circ 0:08 0:12 4 pdiff_8 0:28 0:32 4 msualg_7 0:10 0:14 4 msscyc_1 0:14 0:18 4 msaterm 0:15 0:19 4 metrizts 0:17 0:21 4 mesfunc6 0:12 0:16 4 mesfunc2 0:14 0:18 4 matrixr2 0:42 0:46 4 lopban_1 0:49 0:53 4 jordan5d 0:26 0:30 4 jordan24 0:08 0:12 4 jordan1e 0:14 0:18 4 integra2 0:18 0:22 4 integr10 0:07 0:11 4 int_5 1:14 1:18 4 gobrd13 0:26 0:30 4 glib_004 0:49 0:53 4 functor1 0:05 0:09 4 freealg 0:14 0:18 4 finseq_6 0:10 0:14 4 finseq_5 0:05 0:09 4 fib_num4 0:13 0:17 4 euclid_4 0:10 0:14 4 clopban1 0:49 0:53 4 card_3 0:04 0:08 4 bcialg_5 0:04 0:08 4 amistd_3 0:07 0:11 4 altcat_1 0:04 0:08 4 zf_refle 0:04 0:07 3 zf_lang 0:05 0:08 3 yellow_7 0:07 0:10 3 yellow21 0:06 0:09 3 yellow10 0:07 0:10 3 wellfnd1 0:02 0:05 3 waybel_3 0:06 0:09 3 waybel_2 0:08 0:11 3 waybel21 0:09 0:12 3 waybel17 0:09 0:12 3 vfunct_1 0:08 0:11 3 vectsp_5 0:06 0:09 3 valued_1 0:14 0:17 3 unialg_2 0:05 0:08 3 tsep_1 0:03 0:06 3 trees_1 0:06 0:09 3 topreal7 0:09 0:12 3 topgrp_1 0:05 0:08 3 topdim_1 0:12 0:15 3 sfmastr3 1:08 1:11 3 scmring2 0:05 0:08 3 rusub_2 0:07 0:10 3 rusub_1 0:08 0:11 3 rlvect_3 0:04 0:07 3 rlsub_2 0:06 0:09 3 rfunct_2 0:09 0:12 3 pencil_4 0:05 0:08 3 pencil_1 0:06 0:09 3 pdiff_6 0:40 0:43 3 pboole 0:02 0:05 3 ordinal5 0:06 0:09 3 mycielsk 0:11 0:14 3 msualg_2 0:07 0:10 3 msafree 0:14 0:17 3 mfold_1 0:35 0:38 3 mesfun6c 0:15 0:18 3 limfunc3 0:20 0:23 3 lexbfs 1:10 1:13 3 latsubgr 0:07 0:10 3 jordan8 0:09 0:12 3 jordan1d 0:15 0:18 3 jordan10 0:10 0:13 3 jordan1 0:16 0:19 3 integr14 0:09 0:12 3 hahnban1 0:10 0:13 3 group_6 0:08 0:11 3 group_2 0:08 0:11 3 funct_2 0:02 0:05 3 ftacell1 4:08 4:11 3 fsm_2 0:05 0:08 3 fintopo6 0:10 0:13 3 finsop_1 0:04 0:07 3 filter_2 0:20 0:23 3 fdiff_5 0:16 0:19 3 ens_1 0:15 0:18 3 complfld 0:02 0:05 3 coh_sp 0:05 0:08 3 catalan1 0:02 0:05 3 c0sp2 0:40 0:43 3 borsuk_1 0:08 0:11 3 ami_wstd 0:14 0:17 3 zfrefle1 0:02 0:04 2 yellow12 0:04 0:06 2 waybel_9 0:08 0:10 2 waybel_1 0:07 0:09 2 waybel30 0:09 0:11 2 waybel24 0:07 0:09 2 waybel19 0:08 0:10 2 waybel11 0:13 0:15 2 waybel10 0:12 0:14 2 vfunct_2 0:05 0:07 2 vectsp_8 0:10 0:12 2 vectsp_4 0:04 0:06 2 urysohn1 0:03 0:05 2 topreala 0:08 0:10 2 topalg_2 0:07 0:09 2 taylor_2 0:15 0:17 2 substut1 0:17 0:19 2 simplex2 1:25 1:27 2 sfmastr1 0:29 0:31 2 setwop_2 0:04 0:06 2 seqfunc 0:08 0:10 2 scmring4 0:26 0:28 2 scmfsa8c 1:27 1:29 2 scheme1 0:03 0:05 2 rvsum_1 0:24 0:26 2 rusub_4 0:05 0:07 2 rsspace 0:07 0:09 2 roughs_1 0:07 0:09 2 rmod_3 0:04 0:06 2 rltopsp1 0:07 0:09 2 rlsub_1 0:04 0:06 2 rinfsup1 0:12 0:14 2 quatern3 1:34 1:36 2 quatern2 1:36 1:38 2 partit_2 0:02 0:04 2 numbers 0:02 0:04 2 ndiff_5 2:48 2:50 2 ndiff_4 0:49 0:51 2 ncfcont1 0:20 0:22 2 msualg_4 0:05 0:07 2 msualg_3 0:06 0:08 2 modelc_1 0:16 0:18 2 member_1 0:04 0:06 2 measure6 0:13 0:15 2 measure3 0:06 0:08 2 mcart_1 0:01 0:03 2 lopclset 0:04 0:06 2 lopban_5 0:17 0:19 2 lattice3 0:03 0:05 2 lang1 0:04 0:06 2 knaster 0:06 0:08 2 jordan1k 0:08 0:10 2 jordan18 0:04 0:06 2 jgraph_4 1:35 1:37 2 jct_misc 0:10 0:12 2 int_6 0:15 0:17 2 instalg1 0:13 0:15 2 group_5 0:06 0:08 2 group_3 0:05 0:07 2 graphsp 0:20 0:22 2 goedelcp 0:08 0:10 2 glib_000 0:12 0:14 2 funct_8 0:13 0:15 2 funct_6 0:04 0:06 2 funct_4 0:02 0:04 2 finseq_7 0:05 0:07 2 finseq_2 0:10 0:12 2 fcont_3 0:19 0:21 2 conlat_2 0:09 0:11 2 comseq_1 0:05 0:07 2 complex1 0:05 0:07 2 commacat 0:03 0:05 2 circled1 0:05 0:07 2 cfunct_1 0:09 0:11 2 cfcont_1 0:10 0:12 2 c0sp1 0:36 0:38 2 boolmark 0:03 0:05 2 birkhoff 0:05 0:07 2 bintree2 0:04 0:06 2 binarith 0:29 0:31 2 autalg_1 0:05 0:07 2 alg_1 0:06 0:08 2 zf_fund2 0:03 0:04 1 yellow_3 0:04 0:05 1 yellow_1 0:04 0:05 1 yellow19 0:04 0:05 1 yellow17 0:01 0:02 1 yellow14 0:04 0:05 1 xxreal_1 0:03 0:04 1 xxreal_0 0:00 0:01 1 wsierp_1 0:12 0:13 1 wellord1 0:01 0:02 1 waybel_7 0:05 0:06 1 waybel_4 0:08 0:09 1 waybel35 0:02 0:03 1 waybel33 0:07 0:08 1 waybel32 0:03 0:04 1 waybel28 0:02 0:03 1 waybel23 0:06 0:07 1 waybel20 0:13 0:14 1 waybel14 0:07 0:08 1 waybel12 0:06 0:07 1 vectsp_7 0:02 0:03 1 vectsp_2 0:03 0:04 1 valued_0 0:04 0:05 1 urysohn2 0:06 0:07 1 turing_1 0:23 0:24 1 tsep_2 0:00 0:01 1 trees_a 0:01 0:02 1 trees_4 0:06 0:07 1 tex_2 0:04 0:05 1 tdlat_3 0:01 0:02 1 tdlat_1 0:04 0:05 1 tbsp_1 0:04 0:05 1 t_0topsp 0:01 0:02 1 supinf_2 0:07 0:08 1 substlat 0:01 0:02 1 subset_1 0:00 0:01 1 square_1 0:01 0:02 1 sprect_5 0:04 0:05 1 sincos10 0:19 0:20 1 sin_cos7 0:26 0:27 1 series_1 0:15 0:16 1 seqm_3 0:12 0:13 1 seq_1 0:05 0:06 1 scmpds_i 0:05 0:06 1 scmpds_6 0:47 0:48 1 scmpds_5 0:18 0:19 1 scmp_gcd 0:12 0:13 1 scmfsa_7 0:14 0:15 1 scm_1 0:06 0:07 1 rusub_5 0:03 0:04 1 rpr_1 0:02 0:03 1 rmod_2 0:04 0:05 1 ring_1 0:03 0:04 1 rfinseq2 0:07 0:08 1 rewrite1 0:05 0:06 1 relat_1 0:01 0:02 1 realset2 0:04 0:05 1 real_3 0:28 0:29 1 rat_1 0:02 0:03 1 random_2 0:33 0:34 1 quantal1 0:04 0:05 1 qc_lang4 0:05 0:06 1 prvect_1 0:05 0:06 1 projpl_1 0:01 0:02 1 prob_4 0:12 0:13 1 pralg_2 0:04 0:05 1 polyalg1 0:07 0:08 1 pencil_2 0:07 0:08 1 pdiff_3 0:11 0:12 1 pcomps_2 0:04 0:05 1 partfun1 0:01 0:02 1 ordinal4 0:01 0:02 1 ordinal2 0:01 0:02 1 orders_3 0:01 0:02 1 orders_2 0:02 0:03 1 orders_1 0:03 0:04 1 openlatt 0:02 0:03 1 normform 0:03 0:04 1 nfcont_4 0:12 0:13 1 nfcont_3 0:09 0:10 1 nfcont_1 0:05 0:06 1 msualg_1 0:02 0:03 1 mssubfam 0:02 0:03 1 msafree2 0:07 0:08 1 mod_3 0:03 0:04 1 mmlquery 0:05 0:06 1 metric_6 0:02 0:03 1 metric_1 0:03 0:04 1 mesfunc9 0:29 0:30 1 mesfunc8 0:15 0:16 1 mesfunc7 0:09 0:10 1 mesfun9c 0:16 0:17 1 measure1 0:04 0:05 1 matroid0 0:07 0:08 1 matrix_8 0:03 0:04 1 matrix_4 0:05 0:06 1 matrix_1 0:07 0:08 1 mathmorp 0:03 0:04 1 margrel1 0:03 0:04 1 ltlaxio1 0:14 0:15 1 lmod_7 0:04 0:05 1 limfunc2 0:27 0:28 1 lfuzzy_0 0:06 0:07 1 lattice4 0:02 0:03 1 kurato_2 0:09 0:10 1 jordan1c 0:09 0:10 1 jordan16 0:05 0:06 1 interva1 0:03 0:04 1 integra3 1:26 1:27 1 integr1c 0:41 0:42 1 integr18 0:03 0:04 1 int_7 0:46 0:47 1 int_1 0:01 0:02 1 incsp_1 0:02 0:03 1 hilbert2 0:10 0:11 1 heyting1 0:04 0:05 1 henmodel 0:09 0:10 1 hausdorf 0:03 0:04 1 hallmar1 0:04 0:05 1 grsolv_1 0:06 0:07 1 group_8 0:05 0:06 1 grnilp_1 0:12 0:13 1 grfunc_1 0:00 0:01 1 graph_5 0:20 0:21 1 graph_4 0:08 0:09 1 goboard4 0:25 0:26 1 glib_002 0:13 0:14 1 glib_001 0:54 0:55 1 fuzzy_4 0:07 0:08 1 functor3 0:09 0:10 1 funct_5 0:02 0:03 1 funct_1 0:01 0:02 1 funcop_1 0:02 0:03 1 frechet 0:08 0:09 1 flang_2 0:03 0:04 1 finseq_8 0:04 0:05 1 filter_0 0:03 0:04 1 fib_num 0:07 0:08 1 fdiff_9 0:12 0:13 1 euclid_8 0:38 0:39 1 euclid 0:11 0:12 1 eqrel_1 0:05 0:06 1 entropy1 0:25 0:26 1 ec_pf_1 1:13 1:14 1 csspace2 0:19 0:20 1 convex3 0:06 0:07 1 closure2 0:03 0:04 1 clopban2 0:31 0:32 1 cayley 0:02 0:03 1 cat_4 0:07 0:08 1 card_fil 0:02 0:03 1 card_5 0:03 0:04 1 card_1 0:01 0:02 1 calcul_2 0:05 0:06 1 bvfunc_9 0:06 0:07 1 bvfunc_8 0:01 0:02 1 bvfunc_2 0:03 0:04 1 bvfunc26 0:02 0:03 1 bvfunc11 0:01 0:02 1 brouwer2 0:58 0:59 1 borsuk_4 0:15 0:16 1 bor_cant 0:52 0:53 1 bcialg_2 0:03 0:04 1 bcialg_1 0:03 0:04 1 bagorder 0:43 0:44 1 autgroup 0:04 0:05 1 arytm_2 0:02 0:03 1 anproj_1 0:02 0:03 1 analmetr 0:04 0:05 1 amistd_4 0:01 0:02 1 ami_5 0:13 0:14 1 ali2 0:01 0:02 1 algstr_3 0:00 0:01 1 afvect01 0:00 0:01 1 afproj 0:05 0:06 1 abian 0:05 0:06 1 zfmisc_1 0:01 0:01 0 zf_model 0:02 0:02 0 zf_colla 0:01 0:01 0 yellow_8 0:01 0:01 0 yellow_6 0:14 0:14 0 yellow_5 0:01 0:01 0 yellow_4 0:01 0:01 0 yellow_2 0:02 0:02 0 yellow_0 0:02 0:02 0 yellow13 0:03 0:03 0 xxreal_3 0:03 0:03 0 xxreal_2 0:02 0:02 0 xtuple_0 0:00 0:00 0 xregular 0:00 0:00 0 xreal_1 0:02 0:02 0 xreal_0 0:01 0:01 0 xcmplx_1 0:01 0:01 0 xcmplx_0 0:01 0:01 0 xboolean 0:07 0:07 0 xboole_1 0:00 0:00 0 xboole_0 0:00 0:00 0 wellset1 0:01 0:01 0 wellord2 0:01 0:01 0 waybel_8 0:05 0:05 0 waybel_5 0:20 0:20 0 waybel_0 0:03 0:03 0 waybel31 0:05 0:05 0 waybel22 0:08 0:08 0 waybel16 0:03 0:03 0 waybel15 0:06 0:06 0 waybel13 0:09 0:09 0 vectsp_9 0:13 0:13 0 vectsp_1 0:03 0:03 0 valuat_1 0:07 0:07 0 urysohn3 0:08 0:08 0 uniform1 0:07 0:07 0 unialg_3 0:07 0:07 0 unialg_1 0:01 0:01 0 twoscomp 0:11 0:11 0 tsp_2 0:03 0:03 0 tsp_1 0:01 0:01 0 treal_1 0:07 0:07 0 transgeo 0:03 0:03 0 tops_4 0:06 0:06 0 tops_3 0:01 0:01 0 tops_2 0:03 0:03 0 tops_1 0:01 0:01 0 topreal8 0:09 0:09 0 topreal5 0:04 0:04 0 topmetr3 0:07 0:07 0 topmetr2 0:03 0:03 0 topmetr 0:03 0:03 0 topgen_4 0:03 0:03 0 topgen_2 0:03 0:03 0 topgen_1 0:01 0:01 0 toler_1 0:01 0:01 0 tex_4 0:03 0:03 0 tex_3 0:02 0:02 0 tex_1 0:02 0:02 0 termord 0:10 0:10 0 tdlat_2 0:05 0:05 0 tdgroup 0:01 0:01 0 taxonom2 0:01 0:01 0 taxonom1 0:02 0:02 0 t_1topsp 0:01 0:01 0 sysrel 0:01 0:01 0 symsp_1 0:02 0:02 0 supinf_1 0:00 0:00 0 substut2 0:04 0:04 0 subset 0:00 0:00 0 struct_0 0:00 0:00 0 sppol_1 0:26 0:26 0 sin_cos9 0:22 0:22 0 sin_cos5 0:08 0:08 0 sheffer2 0:01 0:01 0 sheffer1 0:01 0:01 0 sgraph1 0:03 0:03 0 sfmastr2 0:24 0:24 0 setwiseo 0:02 0:02 0 setlim_2 0:03 0:03 0 setlim_1 0:03 0:03 0 setfam_1 0:00 0:00 0 semi_af1 0:02 0:02 0 scpisort 0:36 0:36 0 scmringi 0:06 0:06 0 scmring1 0:03 0:03 0 scmpds_8 0:38 0:38 0 scmpds_3 0:05 0:05 0 scmpds_1 0:01 0:01 0 scmisort 2:10 2:10 0 scmfsa_9 1:04 1:04 0 scmfsa_5 0:08 0:08 0 scmfsa_3 0:08 0:08 0 scmfsa_1 0:05 0:05 0 scmfsa9a 1:01 1:01 0 scmfsa8b 0:44 0:44 0 scmfsa8a 0:29 0:29 0 scmfsa6c 0:19 0:19 0 scmfsa6b 0:20 0:20 0 schems_1 0:00 0:00 0 rsspace3 0:12 0:12 0 rsspace2 0:10 0:10 0 rolle 0:08 0:08 0 robbins3 0:03 0:03 0 robbins2 0:01 0:01 0 robbins1 0:04 0:04 0 rlvect_x 0:07 0:07 0 rlvect_5 0:14 0:14 0 rlvect_1 0:08 0:08 0 ringcat1 0:03 0:03 0 rinfsup2 0:08 0:08 0 rfunct_4 0:12 0:12 0 rewrite3 0:09 0:09 0 rewrite2 0:03 0:03 0 relset_2 0:02 0:02 0 relset_1 0:00 0:00 0 relat_2 0:00 0:00 0 recdef_2 0:02 0:02 0 recdef_1 0:06 0:06 0 realset3 0:01 0:01 0 realset1 0:00 0:00 0 real_ns1 0:19 0:19 0 real_lat 0:02 0:02 0 real_1 0:00 0:00 0 real 0:00 0:00 0 rcomp_1 0:04 0:04 0 ramsey_1 0:12 0:12 0 radix_6 0:02 0:02 0 radix_5 0:03 0:03 0 radix_4 0:05 0:05 0 radix_3 0:05 0:05 0 radix_2 0:09 0:09 0 radix_1 0:06 0:06 0 quin_1 0:04 0:04 0 qmax_1 0:03 0:03 0 qc_lang3 0:02 0:02 0 pzfmisc1 0:01 0:01 0 pythtrip 0:04 0:04 0 prvect_3 0:52 0:52 0 prvect_2 0:16 0:16 0 projred2 0:01 0:01 0 projred1 0:01 0:01 0 projdes1 0:00 0:00 0 procal_1 0:00 0:00 0 prob_2 0:05 0:05 0 prob_1 0:03 0:03 0 prgcor_2 0:05 0:05 0 prepower 0:23 0:23 0 pre_topc 0:01 0:01 0 pre_ff 0:03 0:03 0 power 0:05 0:05 0 poset_1 0:06 0:06 0 polynom8 0:10 0:10 0 polynom4 0:10 0:10 0 polyeq_1 0:08 0:08 0 petri_2 0:05 0:05 0 petri 0:01 0:01 0 pdiff_2 0:27 0:27 0 pdiff_1 0:35 0:35 0 pcomps_1 0:03 0:03 0 pasch 0:01 0:01 0 partit1 0:02 0:02 0 partfun4 0:02 0:02 0 partfun3 0:05 0:05 0 partfun2 0:01 0:01 0 parsp_2 0:03 0:03 0 parsp_1 0:01 0:01 0 pardepap 0:00 0:00 0 papdesaf 0:01 0:01 0 osalg_3 0:02 0:02 0 osalg_2 0:06 0:06 0 osalg_1 0:03 0:03 0 ortsp_1 0:02 0:02 0 ordinal3 0:01 0:01 0 ordinal1 0:01 0:01 0 orders_4 0:03 0:03 0 oposet_1 0:01 0:01 0 o_ring_1 0:04 0:04 0 numerals 0:00 0:00 0 normsp_2 0:06 0:06 0 normsp_1 0:04 0:04 0 normsp_0 0:00 0:00 0 nfcont_2 0:07 0:07 0 net_1 0:00 0:00 0 neckla_2 0:04 0:04 0 ndiff_2 0:13 0:13 0 ncfcont2 0:13 0:13 0 nat_lat 0:02 0:02 0 nat_d 0:02 0:02 0 nat_2 0:05 0:05 0 multop_1 0:00 0:00 0 msafree1 0:03 0:03 0 morph_01 0:02 0:02 0 modcat_1 0:02 0:02 0 mod_4 0:10 0:10 0 mod_2 0:05 0:05 0 midsp_3 0:02 0:02 0 midsp_2 0:01 0:01 0 midsp_1 0:01 0:01 0 metric_3 0:07 0:07 0 metric_2 0:01 0:01 0 mesfunc1 0:08 0:08 0 mesfun10 0:14 0:14 0 membered 0:00 0:00 0 measure5 0:01 0:01 0 measure4 0:05 0:05 0 measure2 0:03 0:03 0 mboolean 0:01 0:01 0 matrprob 0:18 0:18 0 matrlin 0:21 0:21 0 matrixr1 0:09 0:09 0 matrixc1 0:15 0:15 0 matrix_5 0:02 0:02 0 matrix_3 0:14 0:14 0 matrix_2 0:04 0:04 0 matrix17 0:06 0:06 0 matrix16 0:16 0:16 0 matrix12 0:05 0:05 0 lukasi_1 0:01 0:01 0 lp_space 0:16 0:16 0 lopban_4 0:15 0:15 0 lopban_3 0:19 0:19 0 lopban_2 0:27 0:27 0 lmod_6 0:01 0:01 0 lmod_5 0:02 0:02 0 limfunc4 0:14 0:14 0 lattices 0:01 0:01 0 lattice7 0:02 0:02 0 lattice6 0:06 0:06 0 lattice2 0:02 0:02 0 latsum_1 0:01 0:01 0 laplace 0:43 0:43 0 l_hospit 0:16 0:16 0 kurato_1 0:04 0:04 0 kurato_0 0:02 0:02 0 jordan2b 0:08 0:08 0 jordan22 0:32 0:32 0 jordan20 0:39 0:39 0 jordan1i 0:18 0:18 0 jordan1f 0:11 0:11 0 jordan1b 0:10 0:10 0 jordan17 0:03 0:03 0 jordan14 0:25 0:25 0 jgraph_7 0:47 0:47 0 isomichi 0:03 0:03 0 irrat_1 0:12 0:12 0 intpro_1 0:03 0:03 0 integra8 0:15 0:15 0 integra7 0:14 0:14 0 integra6 0:29 0:29 0 int_2 0:01 0:01 0 incproj 0:01 0:01 0 idea_1 0:22 0:22 0 homothet 0:01 0:01 0 hilbert1 0:01 0:01 0 hilbasis 1:28 1:28 0 heyting3 0:10 0:10 0 heyting2 0:04 0:04 0 hessenbe 0:00 0:00 0 heine 0:06 0:06 0 groupp_1 0:05 0:05 0 group_12 0:06 0:06 0 group_11 0:01 0:01 0 group_1 0:04 0:04 0 groeb_3 0:41 0:41 0 groeb_2 0:35 0:35 0 grcat_1 0:06 0:06 0 graph_1 0:07 0:07 0 gr_cy_2 0:04 0:04 0 gr_cy_1 0:13 0:13 0 goboard8 0:12 0:12 0 goboard7 0:44 0:44 0 gfacirc2 0:25 0:25 0 geomtrap 0:09 0:09 0 genealg1 0:11 0:11 0 gate_5 1:39 1:39 0 gate_4 0:01 0:01 0 gate_3 0:02 0:02 0 gate_2 0:00 0:00 0 gate_1 0:01 0:01 0 fvsum_1 0:07 0:07 0 fuzzy_2 0:06 0:06 0 fuzzy_1 0:05 0:05 0 functor2 0:04 0:04 0 funct_3 0:02 0:02 0 funcsdom 0:04 0:04 0 fsm_3 0:08 0:08 0 frechet2 0:08 0:08 0 fraenkel 0:01 0:01 0 flang_3 0:02 0:02 0 flang_1 0:03 0:03 0 fintopo5 0:03 0:03 0 fintopo4 0:02 0:02 0 fintopo3 0:01 0:01 0 fintopo2 0:01 0:01 0 finsub_1 0:00 0:00 0 finset_1 0:01 0:01 0 finseqop 0:07 0:07 0 finance1 0:06 0:06 0 fin_topo 0:02 0:02 0 filerec1 0:05 0:05 0 fib_num3 0:06 0:06 0 fib_fusc 0:05 0:05 0 ff_siec 0:01 0:01 0 fdiff_8 0:12 0:12 0 fdiff_10 0:09 0:09 0 fcont_2 0:11 0:11 0 extreal2 0:01 0:01 0 euclmetr 0:02 0:02 0 euclidlp 0:13 0:13 0 euclid_5 0:04 0:04 0 euclid_2 0:05 0:05 0 ec_pf_2 0:30 0:30 0 e_siec 0:01 0:01 0 dynkin 0:01 0:01 0 domain_1 0:01 0:01 0 dirort 0:01 0:01 0 diraf 0:01 0:01 0 diff_3 0:36 0:36 0 diff_2 0:17 0:17 0 diff_1 0:18 0:18 0 csspace3 0:14 0:14 0 csspace 0:17 0:17 0 cqc_the3 0:02 0:02 0 cqc_the2 0:02 0:02 0 cqc_lang 0:03 0:03 0 convfun1 0:21 0:21 0 convex2 0:12 0:12 0 connsp_2 0:01 0:01 0 connsp_1 0:02 0:02 0 conmetr1 0:02 0:02 0 conmetr 0:02 0:02 0 conaffm 0:01 0:01 0 comseq_3 0:16 0:16 0 comseq_2 0:06 0:06 0 compts_1 0:02 0:02 0 compos_2 0:08 0:08 0 complsp2 0:24 0:24 0 complsp1 0:02 0:02 0 compact1 0:03 0:03 0 collsp 0:00 0:00 0 clvect_3 0:12 0:12 0 clvect_2 0:08 0:08 0 closure3 0:03 0:03 0 clopban4 0:17 0:17 0 clopban3 0:18 0:18 0 classes2 0:01 0:01 0 classes1 0:02 0:02 0 circcmb2 0:05 0:05 0 cgames_1 0:05 0:05 0 cfuncdom 0:02 0:02 0 cat_3 0:04 0:04 0 cat_2 0:07 0:07 0 cat_1 0:03 0:03 0 card_lar 0:01 0:01 0 cantor_1 0:01 0:01 0 bvfunc_7 0:02 0:02 0 bvfunc_4 0:03 0:03 0 bvfunc_3 0:02 0:02 0 bvfunc25 0:01 0:01 0 borsuk_3 0:03 0:03 0 boolealg 0:01 0:01 0 boole 0:00 0:00 0 bintree1 0:07 0:07 0 binop_2 0:01 0:01 0 binop_1 0:01 0:01 0 binom 0:08 0:08 0 binari_4 0:10 0:10 0 binari_3 0:04 0:04 0 binari_2 0:36 0:36 0 bhsp_7 0:02 0:02 0 bhsp_6 0:05 0:05 0 bhsp_5 0:04 0:04 0 bhsp_4 0:12 0:12 0 bhsp_3 0:04 0:04 0 bhsp_2 0:03 0:03 0 bhsp_1 0:05 0:05 0 bciideal 0:01 0:01 0 bcialg_4 0:03 0:03 0 bcialg_3 0:01 0:01 0 axioms 0:00 0:00 0 arytm_3 0:01 0:01 0 arytm_1 0:00 0:00 0 arytm_0 0:02 0:02 0 arrow 0:02 0:02 0 armstrng 0:29 0:29 0 arithm 0:00 0:00 0 aofa_000 2:13 -133 analort 0:03 0:03 0 analoaf 0:03 0:03 0 ami_4 0:07 0:07 0 ami_3 0:10 0:10 0 ami_2 0:04 0:04 0 algstr_4 0:25 0:25 0 algstr_2 0:02 0:02 0 algstr_1 0:02 0:02 0 algstr_0 0:00 0:00 0 algseq_1 0:00 0:00 0 afvect0 0:02 0:02 0 aff_4 0:01 0:01 0 aff_3 0:01 0:01 0 aff_2 0:01 0:01 0 aff_1 0:00 0:00 0 absvalue 0:01 0:01 0 vectsp11 0:57 0:56 -1 translac 0:02 0:01 -1 toprns_1 0:09 0:08 -1 sprect_4 0:22 0:21 -1 series_4 0:14 0:13 -1 scpinvar 1:06 1:05 -1 scmpds_2 0:28 0:27 -1 ratfunc1 0:29 0:28 -1 polyred 0:49 0:48 -1 polynom7 0:13 0:12 -1 polynom2 0:40 0:39 -1 nagata_1 0:17 0:16 -1 msualg_5 0:11 0:10 -1 msscyc_2 0:17 0:16 -1 measure8 0:21 0:20 -1 matrix_6 0:05 0:04 -1 integra5 0:21 0:20 -1 integra4 0:35 0:34 -1 gr_cy_3 0:07 0:06 -1 fscirc_1 0:12 0:11 -1 extreal1 0:11 0:10 -1 dickson 0:32 0:31 -1 connsp_3 0:02 0:01 -1 conlat_1 0:07 0:06 -1 compl_sp 0:24 0:23 -1 bvfunc_5 0:02 0:01 -1 bvfunc14 0:24 0:23 -1 asympt_1 1:31 1:30 -1 altcat_3 0:02 0:01 -1 polyeq_4 0:08 0:06 -2 decomp_1 0:05 0:03 -2 yoneda_1 0:17 0:14 -3 prgcor_1 0:12 0:09 -3 nat_5 0:46 0:43 -3 bvfunc_6 0:27 0:24 -3 bvfunc10 0:22 0:18 -4 msuhom_1 0:14 0:09 -5 sin_cos8 0:21 0:15 -6 polyeq_3 0:46 0:40 -6 integra9 0:30 0:24 -6 pepin 0:20 0:13 -7 jordan4 0:50 0:43 -7 jordan3 0:57 0:50 -7 asympt_0 0:43 0:35 -8 taylor_1 0:44 0:35 -9 msualg_8 0:24 0:14 -10 euler_2 0:35 0:25 -10 gobrd10 0:19 0:07 -12 polyeq_2 0:23 0:08 -15 int_3 0:37 0:22 -15 fdiff_4 0:39 0:24 -15 series_3 0:51 0:35 -16 fdiff_7 0:31 0:13 -18 comptrig 0:54 0:35 -19 weddwitt 1:07 0:47 -20 lpspace1 0:52 0:30 -22 simplex0 0:52 0:27 -25 fdiff_6 1:02 0:29 -33 series_5 1:02 0:26 -36 ----- Koniec przekazanej wiadomości ----- </pre> trybulec< at >math.uwb.edu.pl 2012-03-12T11:48:34 Urelements? 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 disgusting. Verifying some articles becomes longer by more than two orders. One of the reason was the lack of the type discipline. If e.g. 'x &lt;&gt; y' is among premises the poor thing will append to premises both 'not x c= y' and 'not y c= x' even when x and y are real numbers and such inclusions are (almost) meaningless. Therefore it is necessary to recover the old root type, under the new name 'element'. When identifying 'Any' and 'set' was easy, going back is a little bit harder. The first obvious step was done (by Czeslaw and Artur): i. in HIDDEN the mode 'element' is introduced and it is the mother type of the mode 'set'. The equality is introduced for elements, but the membership needs the second argument to be a set. ii. default types for numerals and structures are put to 'set' (temporarily) iii. when in the functor or mode definition qualification was empty, it was by default set, it was necessary, again for a while, to insert the qualification '-&gt; set'. We should now discuss what should be a set, and what should not. E.g. ordered pairs are probably elements, not sets? Regards, Andrzej </pre> trybulec< at >math.uwb.edu.pl 2012-03-11T17:21:52 How to call it? 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 lstlangmizar.sty 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 Call for papers: THedu'12 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 (DGS). The workshop tries to combine and focus systems of these areas to enhance existing educational software as well as studying the design of the next generation of mechanised mathematics assistants (MMA). Elements for next-generation MMA's include: * Declarative Languages for Problem Solution: education in applied sciences and in engineering is mainly concerned with problems, which involve operations on elementary objects to be transformed to an object representing a problem solution. Preconditions and postconditions of these operations can be used to describe the possible steps in the problem space; thus, ATP-systems can be used to check if an operation sequence given by the user does actually present a problem solution. Such "Problem Solution Languages" encompass declarative proof languages like Isabelle/Isar or Coq's Mathematical Proof Language, but also more specialized forms such as, for example, geometric problem solution languages that express a proof argument in Euklidian Geometry or languages for graph theory. * Consistent Mathematical Content Representation: Libraries of existing ITP-Systems, in particular those following the LCF-prover paradigm, usually provide logically coherent and human readable knowledge. In the leading provers, mathematical knowledge is covered to an extent beyond most courses in applied sciences. However, the potential of this mechanised knowledge for education is clearly not yet recognised adequately: renewed pedagogy calls for inquiry-based learning from concrete to abstract --- and the knowledge's logical coherence supports such learning: for instance, the formula 2.pi depends on the definition of reals and of multiplication; close to these definitions are the laws like commutativity etc. However, the complexity of the knowledge's traceable interrelations poses a challenge to usability design. * User-Guidance in Stepwise Problem Solving: Such guidance is indispensable for independent learning, but costly to implement so far, because so many special cases need to be coded by hand. However, TP technology makes automated generation of user-guidance reachable: declarative languages as mentioned above, novel programming languages combining computation and deduction, methods for automated construction with ruler and compass from specifications, etc --- all these methods 'know how to solve a problem'; so, use the methods' knowledge to generate user-guidance mechanically, this is an appealing challenge for ATP and ITP, and probably for compiler construction! In principle, mathematical software can be conceived as models of mathematics: The challenge addressed by this workshop series is to provide appealing models for MMAs which are interactive and which explain themselves such that interested students can independently learn by inquiry and experimentation. Program Committee ----------------- Ralph-Johan Back, Abo University, Turku, Finland Francisco Botana, University of Vigo at Pontevedra, Spain Florian Haftman, Munich University of Technology, Germany Predrag Janicic, University of Belgrade, Serbia Cezary Kaliszyk, University of Tsukuba, Japan Julien Narboux, University of Strasbourg, France Filip Maric, University of Belgrade, Serbia Walther Neuper, Graz University of Technology, Austria Pedro Quaresma, University of Coimbra, Portugal Wolfgang Schreiner, Johannes Kepler University, Linz, Austria Laurent Th??ry, Sophia Antipolis, INRIA, France Makarius Wenzel, University Paris-Sud, France Burkhart Wolff, University Paris-Sud, France Important Dates (by easychair) --------------- * Extended Abstracts/Demo proposals: 01 May 2012 * Author Notification: 01 Jun 2012 * Final Version: 15 Jun 2012 * Worshop Day: 11 Jul 2012 Submission ---------- We welcome submission of proposals to present a demo, as well as submissions of extended abstracts (8 pages max) presenting original unpublished work which is not been submitted for publication elsewhere. Selected extended abstracts will appear in CISUC Technical Report series (ISSN 0874-338X, [1]). All accepted extended abstracts and system demos will be presented at the workshop, and the extended abstracts will be made available online. A publication post-proceedings (papers, 15 pages max) under EPTCS is under consideration. Extended abstracts and demo proposals should be submitted via THedu'12 easychair [2]. Extended abstracts should be no more than 8 pages in length and are to be submitted in PDF format. They must conform to the EPTCS style guidelines [3]. At least one author of each accepted extended abstract/demo is expected to attend THedu'12 and presents her or his extended abstract/demo. [1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/ [2] http://www.easychair.org/conferences/?conf=thedu12 [3] http://http://style.eptcs.org/ </pre> Makarius 2012-02-27T13:20:31 ETAPS Workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012) 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 Paris-Sud) ** Registration ** For non IC0901 participants, registration is done through the ETAPS 2012 registration system (http://www.etaps.org/2012/registration). Regular registration fees end 26 February 2012. </pre> Hugo Herbelin 2012-02-24T22:09:52 New Mizar articles 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 Operations of Points on Elliptic Curve in Projective Coordinates by Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima and Yasunari Shidama Received November 3, 2011 1139. TOPALG_6 Fundamental Group of $n$-sphere for $n \geq 2$ by Marco Riccardi and Artur Korni{\l}owicz Received November 3, 2011 1140. BORSUK_7 The {B}orsuk-Ulam Theorem by Artur Korni{\l}owicz and Marco Riccardi Received November 3, 2011 1141. PDIFF_9 Higher Order Partial Differentiation by Noboru Endou, Hiroyuki Okazaki and Yasunari Shidama Received November 20, 2011 1142. DESCIP_1 Formalization of the Data Encryption Standard by Hiroyuki Okazaki and Yasunari Shidama Received November 30, 2011 1143. MMLQUERY Semantic of MML Query by Grzegorz Bancerek Received December 18, 2011 1144. MENELAUS Routh's, {M}enelaus' and Generalized {C}eva's Theorems by Boris A. Shminke Received January 16, 2012 1145. SCMYCIEL Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph by Piotr Rudnicki and Lorna Stewart Received February 8, 2012 1146. NTALGO_1 Extended Euclidean Algorithm and CRT Algorithm by Hiroyuki Okazaki, Yosiki Aoki and Yasunari Shidama Received February 8, 2012 1147. RATFUNC1 Introduction to Rational Functions by Christoph Schwarzweller Received February 8, 2012 Regards, Adam Grabowski Library Committee of the Association of Mizar Users </pre> Adam Grabowski 2012-02-22T08:13:21 CICM 2012 -- last call for papers (fwd) 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 papers CICM 2012 - Conference on Intelligent Computer Mathematics July 9-13, 2012 at Jacobs University, Bremen, Germany http://www.informatik.uni-bremen.de/cicm2012/ Call for Papers ---------------------------------------------------------------- As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, automated deduction, mathematical publishing and novel user interfaces individually have long and successful histories, we are now seeing increasing opportunities for synergy among these areas. The Conference on Intelligent Computer Mathematics offers a venue for discussing these areas and their synergy. The conference will be organized by Serge Autexier and Michael Kohlhase at Jacobs University in Bremen and consist of five tracks: Artificial Intelligence and Symbolic Computation (AISC) Co-Chairs: John A. Campbell, Jacques Carette Calculemus Chair: Gabriel Dos Reis Digital Mathematical Libraries (DML) Chair: Petr Sojka Mathematical Knowledge Management (MKM) Chair: Makarius Wenzel Systems and Projects Chair: Volker Sorge The overall programme will be organized by the General Program Chair Johan Jeuring. Invited talks will be given by: Yannis Haralambous, Dpartement Informatique, Tlcom Bretagne Conor McBride, Department of Computer and Information Sciences, University of Strathclyde Cezar Ionescu, Potsdam Institute for Climate Impact Research ---------------------------------------------------------------- Important dates ---------------------------------------------------------------- Abstract submission: 20 February 2012 Submission deadline: 26 February 2012 Reviews sent to authors: 23 March 2012 Rebuttals due: 30 March 2012 Notification of acceptance: 6 April 2012 Camera ready copies due: 20 April 2012 Conference: 9-13 July 2012 ---------------------------------------------------------------- Tracks ---------------------------------------------------------------- *** AISC *** Symbolic computation can be roughly described as the study of algorithms which operate on expression trees. Another way to phrase this is to say that the denotational semantics of expressions trees is not fixed, but is rather context dependent. Expression simplification is probably the archetypal symbolic computation. Mathematically oriented software (such as the so-called computer algebra systems) have been doing this for decades, but not long thereafter, systems doing proof planning and theorem discovery also started doing the same; some attempts at knowledge management and 'expert systems' were also symbolic, but less successfully so. More recently, many different kinds of program analyses have gotten `symbolic', as well as some of the automated theorem proving (SMT, CAV, etc). But a large number of the underlying problems solved by symbolic techniques are well known to be undecidable (never mind the many that are EXP-time complete, etc). Artificial Intelligence has been attacking many of these different sub-problems for quite some time, and has also built up a solid body of knowledge. In fact, most symbolic computation systems grew out of AI projects. These two fields definitely intersect. One could say that in the intersection lies all those problems for which we have no decision procedures. In other words, decision procedures mark a definite phase shift in our understanding, but are not always possible. Yet we still want to solve certain problems, and must find 'other' means of (partial) solution. This is the fertile land which comprises the core of AISC. Rather than try to exhaustively list topics of interest, it is simplest to say that AISC seeks work which advances the understanding of Solving problems which fundamentally involve the manipulation of expressions, but for which decision procedures are unlikely to ever exist. *** Calculemus *** Calculemus is a series of conferences dedicated to the integration of computer algebra systems (CAS) and systems for mechanised reasoning, the interactive theorem provers or proof assistants (PA) and the automated theorem provers (ATP). Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanised reasoning) as well as newly emerging ones (on user interfaces, knowledge management, theory exploration, etc.) The main concern of the Calculemus community is to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems for computer mathematics that will routinely be used by mathematicians, computer scientists and engineers in their every day business. The topics of interest of Calculemus include but are not limited to: * Theorem proving in computer algebra (CAS) * Computer algebra in theorem proving (PA and ATP) * Case studies and applications that both involve computer algebra and mechanised reasoning * Representation of mathematics in computer algebra * Adding computational capabilities to PA and ATP * Formal methods requiring mixed computing and proving * Combining methods of symbolic computation and formal deduction * Mathematical computation in PA and ATP * Theory, design and implementation of interdisciplinary systems for computer mathematics * Theory exploration techniques * Input languages, programming languages, types and constraint languages, and modeling languages for mechanised mathematics systems (PA, CAS, and ATP). * Infrastructure for mathematical services *** DML *** Mathematicians dream of a digital archive containing all peer-reviewed mathematical literature ever published, properly linked, validated and verified. It is estimated that the entire corpus of mathematical knowledge published over the centuries does not exceed 100,000,000 pages, an amount easily manageable by current information technologies. Following success of DML 2008, DML 2009 DML 2010, and DML 2011 track objectives are to formulate the strategy and goals of a global mathematical digital library and to summarize the current successes and failures of ongoing technologies and related projects as EuDML, asking such questions as: * What technologies, standards, algorithms and formats should be used and what metadata should be shared? * What business models are suitable for publishers of mathematical literature, authors and funders of their projects and institutions? * Is there a model of sustainable, interoperable, and extensible mathematical library that mathematicians can use in their everyday work? * What is the best practice for * retrodigitized mathematics (from images via OCR to MathML or TeX); * retro-born-digital mathematics (from existing electronic copy in DVI, PS or PDF to MathML or TeX); * born-digital mathematics (how to make needed metadata and file formats available as a side effect of publishing workflow [CEDRAM/Euclid model])? DML is an opportunity to share experience and best practices between projects in any area (MKM, NLP, OCR, pattern recognition, whatever) that could change the paradigm for searching, accessing, and interacting with the mathematical corpus. The track is trans/interdisciplinary and contributions from any kind of people on any aspect of the DML building are welcome. *** MKM *** Mathematical Knowledge Management is an interdisciplinary field of research in the intersection of mathematics, computer science, library science, and scientific publishing. The objective of MKM is to develop new and better ways of managing sophisticated mathematical knowledge, based on innovative technology of computer science, the Internet, and intelligent knowledge processing. MKM is expected to serve mathematicians, scientists, and engineers who produce and use mathematical knowledge; educators and students who teach and learn mathematics; publishers who offer mathematical textbooks and disseminate new mathematical results; and librarians and mathematicians who catalog and organize mathematical knowledge. The conference is concerned with all aspects of mathematical knowledge management. A non-exclusive list of important topics includes: * Representations of mathematical knowledge * Authoring languages and tools * Repositories of formalized mathematics * Deduction systems * Mathematical digital libraries * Diagrammatic representations * Mathematical OCR * Mathematical search and retrieval * Math assistants, tutoring and assessment systems * MathML, OpenMath, and other mathematical content standards * Web presentation of mathematics * Data mining, discovery, theory exploration * Computer algebra systems * Collaboration tools for mathematics * Challenges and solutions for mathematical workflows *** Systems and Projects *** The Systems and Projects track of the Conferences on Intelligent Computer Mathematics is a forum for presentation of systems and new and ongoing projects in all areas and topics related to the CICM conferences: * AI and Symbolic Computation * Deduction and Computer Algebra * Mathematical Knowledge Management * Digital Mathematical Libraries The track aims to provide an overview of the latest developments and trends within the CICM community as well as to exchange ideas between developers and introduce systems to an audience of potential users. We solicit submissions for two page abstracts in the categories of system descriptions and project presentations. System description should present * newly developed systems, * systems that have not previously been presented to the CICM community, or * significant updates to existing systems. Project presentation should describe * projects that are new or about to start, * ongoing projects that have not yet been presented to the CICM community. * significant new developments in ongoing previously presented projects. All submissions should contain links to demos, downloadable systems, or project pages. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted abstracts will be published in the CICM proceedings in Springer's LNAI series. Author's are expected to present their abstracts in 5-10 minute teaser talks followed by an open demo/poster session. System papers must be accompanied by a system demonstration, while project papers must be accompanied by a poster presentation. ---------------------------------------------------------------- Submitting ---------------------------------------------------------------- Submissions to tracks A to D must not exceed 15 pages and will be reviewed and evaluated with respect to relevance, clarity, quality, originality, and impact. Shorter papers, e.g., for system descriptions, are welcome. Authors will have an opportunity to respond to their papers' reviews before the programme committee makes a decision. Submissions to the Systems &amp; Projects track must not exceed four pages. The accepted abstracts will be presented at CICM in a fast presentation session, followed by an open demo/poster session. System papers must be accompanied by a system demonstration, and project papers must be accompanied by a poster presentation. The four pages of the abstract should be new material, accompanied by links to demos/downloads/project-pages and [existing] system descriptions. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted conference submissions from all tracks will be published as a volume in the series Lecture Notes in Artificial Intelligence (LNAI) by Springer. In addition to these formal proceedings, authors are permitted and encouraged to publish the final versions of their papers on arXiv.org. Work-in-progress submissions are intended to provide a forum for the presentation of original work that is not (yet) in a suitable form for submission as a full or system description paper. This includes work in progress and emerging trends. Their size is not limited, but we recommend 5 - 10 pages. The programme committee may offer authors of rejected formal submissions to publish their contributions as work-in-progress papers instead. Depending on the number of work-in-progress papers accepted, they will be presented at the conference either as short talks or as posters. The work-in-progress proceedings will be published as a technical report. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html). By submitting a paper the authors agree that if it is accepted at least one of the authors will attend the conference to present it. Electronic submission is done through easychair (http://www.easychair.org/conferences/?conf=cicm2012). ---------------------------------------------------------------- Program Committees ---------------------------------------------------------------- General chair: Johan Jeuring (Utrecht University and Open Universiteit the Netherlands) AISC track John A. Campbell; University College London, UK; Co-chair Jacques Carette; McMaster University, Canada; Co-chair Serge Autexier; DFKI Bremen, Germany Jacques Calmet; University of Karlsruhe, Germany Jacques Fleuriot; University of Edinburgh, UK Andrea Kohlhase; International University Bremen, Germany Erik Postma; Maplesoft Inc., Canada Alan Sexton; University of Birmingham, UK Chung-chieh Shan; Cornell University, USA. Stephen Watt; University of Western Ontario, Canada Calculemus track Gabriel Dos Reis; Texas A&amp;M University, USA; Chair Andrea Asperti; University of Bologna, Italy Laurent Bernardin; Maplesoft, Canada James Davenport; University of Bath, UK Ruben Gamboa; University of Wyoming, USA Mark Giesbrecht; University of Waterloo, Canada Sumit Gulwani; Microsoft Research, USA John Harrison; Intel, USA Joris van der Hoeven; cole Polytechnique, France Hoon Hong; North Carolina State University, USA Loc Pottier; INRIA, France Wolfgang Windsteiger; RISC, Austria DML track Petr Sojka; Masaryk University, Brno, CZ; Chair Jos Borbinha; Technical University of Lisbon, PT Thierry Bouche; University Grenoble, FR Michael Doob; University of Manitoba, Winnipeg, CA Thomas Fischer; Goettingen University, DE Yannis Haralambous; Tlcom Bretagne, FR Vclav Hlav; Czech Technical University, Prague, CZ Michael Kohlhase; Jacobs University Bremen, DE Janka Chlebkov; Portsmouth University, UK Enrique Macis-Virgs; University of Santiago de Compostela, ES Bruce Miller; NIST, USA Ji Rkosnk; Academy of Sciences, Prague, CZ Eugenio Rocha; University of Aveiro, PT David Ruddy; Cornell University, US Volker Sorge; University of Birmingham, UK Masakazu Suzuki; Kyushu University, JP MKM track Makarius Wenzel; University of Paris-South, France; Chair David Aspinall; University of Edinburgh, Scotland Jeremy Avigad; Carnegie Mellon University, USA Mateja Jamnik; University of Cambridge, UK Cezary Kaliszyk; University of Tsukuba, Japan Manfred Kerber; University of Birmingham, UK Christoph Lth; DFKI Bremen, Germany Adam Naumowicz; University of Biaystok, Poland Jim Pitman; University of California, Berkeley, USA Pedro Quaresma; Universidade de Coimbra, Portugal Florian Rabe; Jacobs University Bremen, Germany Claudio Sacerdoti Coen; University of Bologna, Italy Enrico Tassi; INRIA Saclay, France Freek Wiedijk; Radboud University Nijmegen, The Netherlands Systems &amp; Projects track Volker Sorge; University of Birmingham, UK; Chair Josef Baker; University of Birmingham, UK John Charnley; Imperial College, UK Manuel Kauers; RISC, Austria Koji Nakagawa; Kyushu University, Japan Piotr Rudnicki; University of Alberta, Canada Josef Urban; Radboud University Nijmegen, The Netherlands Richard Zanibbi; Rochester Institute of Technologies, USA _______________________________________________ projects-mkm-ig mailing list projects-mkm-ig&lt; at &gt;lists.jacobs-university.de http://lists.jacobs-university.de/mailman/listinfo/projects-mkm-ig</pre> Adam Naumowicz 2012-02-22T05:34:46 UITP'12: First Call for Papers 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 the forthcoming 10th UITP workshop, we invite contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. Topics covered include, but are not limited to: * Application-specific interaction mechanisms or designs for prover interfaces; * Experiments and evaluation of prover interfaces; * Languages and tools for authoring, exchanging and presenting proof; * Implementation techniques (e.g. web services, custom middleware, DSLs); * Integration of interfaces and tools to explore and construct proof; * Representation and manipulation of mathematical knowledge or objects; * Visualisation of mathematical objects and proof; * System descriptions. Submitted papers should describe previously unpublished work (completed or in progress), and not be longer than twelve pages. We encourage concise but relevant papers. Submissions should be in PDF format, and typeset with the EasyChair LaTeX document class (which can be downloaded from www.easychair.org), or in similar style. Submission will be via EasyChair. All papers will be peer reviewed by members of the programme committee and selected by the organizers in accordance with the referee reports. Proceedings Accepted papers will appear in the workshop proceedings, which will be available in printed form at the workshop. After the workshop, revised papers can be submitted to a postproceedings, which will appear in an archivable electronic format, preferably published open access. Important Dates Submission deadline: 01.05.2012 Acceptance notification: 01.06.2012 Camera-ready copy: 15.06.2012 PC Chairs Christoph Lüth (DFKI, Germany) Cezary Kaliszyk (University of Innsbruck, Austria) The full program committee will be announced soon. More information about the workshop series can be found at the UITP Interest Group web page www.uitp-ig.org. -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/~cek/ </pre> Cezary Kaliszyk 2012-02-02T19:07:52 2nd announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012) 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 * rewriting techniques and heuristics * automatic termination checking * program synthesis At least the first day of the workshop (Saturday 31 March) is organized in coordination with the COST Action IC0901 Rich-Model Toolkit (http://richmodels.org) which explores how to make automated reasoning applicable to a wider range of problems. ** 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 by ** March 5, 2012 ** (but the sooner the better). ** Post-workshop proceedings ** It is planned to edit afterward a special journal issue collecting selected papers on the topic of the workshop. ** 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 Paris-Sud) ** Registration ** For non IC0901 participants, registration is done through the ETAPS 2012 registration system (http://www.etaps.org/2012/registration). Early registration deadline is: 29 January 2012. </pre> Hugo Herbelin 2012-01-25T16:05:59 Search Engine Search the mailing list at Gmane query http://search.gmane.org/?group=$group=gmane.comp.mathematics.mizar