gmane.comp.mathematics.mizar

duplications in MML 7.13.01_4.181.1147

Josef Urban — 2012-05-20T06:46:00

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

ESSLLI 2012 call for participation

A. Herzig — 2012-05-09T15:30:00

********************************************************************************
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)

Re: real number vs. Element of REAL

Artur Kornilowicz — 2012-05-14T12:14:46




We should also remember about 'extended reals'.

SUPINF_1:
  mode R_eal is Element of ExtREAL;

Regards
Artur





==========================================================================

Artur Kornilowicz                          e-mail: arturk< at >math.uwb.edu.pl

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Informatics                   tel. +48 (85) 745-7662
University of Bialystok                    fax. +48 (85) 745-7662
Sosnowa 64, 15-887 Bialystok, Poland

real number vs. Element of REAL

2012-05-11T09:28:25

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

UITP'12: Final Call for Papers

Cezary Kaliszyk — 2012-04-25T14:01:14

[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

Thedu: 2nd Call for papers

Makarius — 2012-04-16T18:25:30

----------------------------------------------------------------------
                           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/

Fwd: CASC-J6 - the CADE ATP System Competition

Josef Urban — 2012-03-30T17:34:07

A part of this year's CASC will be a MZR< at >Turing ATP/AI competition
division (http://www.cs.miami.edu/~tptp/CASC/J6/Design.html#CompetitionDivisions)
based on MML/MPTP mathematical ATP problems. The competition division
will run on June 24 at the Alan Turing Centenary Conference in
Manchester.

Josef

---------- Forwarded message ----------
From: Geoff Sutcliffe <geoff< at >cs.miami.edu>
Date: Fri, Mar 30, 2012 at 6:17 PM
Subject: CASC-J6 - the CADE ATP System Competition
To: Josef.Urban< at >gmail.com


-------------------------------------------------------------------------------

                CASC-J6 - The CADE ATP System Competition

                              to be held at

                The Alan Turing Centenary Conference and
       The 6th International Joint Conference on Automated Reasoning
            Manchester, United Kindom, 22nd June - 1st July 2012

The CADE and IJCAR conferences  are the major forums  for the  presentation of
new research in all aspects of automated deduction.  In order to stimulate ATP
research and system development,  and to expose ATP systems  within and beyond
the ATP community, the CADE ATP System Competition (CASC) is held at each CADE
or  IJCAR conference.  CASC-J6 will be  held in two parts, at the  Alan Turing
Centenary Conference (CASC< at >Turing) and the 6th International Joint  Conference
on Automated Reasoning (the "regular" CASC).

CASC evaluates  the performance  of sound,  fully automatic,  ATP systems. The
evaluation is in terms of:
 + the number of problems solved, and
 + the number of problems solved with a solution output, and
 + the average runtime for problems solved;
in the context of:
 + a bounded number of eligible problems, chosen from the TPTP library, and
 + specified time limits for solution attempts.
Cash and travel prizes  have been donated for  CASC< at >Turing and the ISA and SMO
problem categories of the LTB division.

The competition organizer is Geoff Sutcliffe. The competition is overseen by a
panel of  knowledgeable researchers  who are not participating  in the  event.
Further details and registration information are available at:
   http://www.tptp.org/CASC/J6/

Registration of systems for CASC-J6 is now invited. System registration closes
on 14th May. Please register early so that adequate resources can be allocated.
    DO IT NOW!  DO IT NOW! DO IT NOW!  DO IT NOW! DO IT NOW! DO IT NOW!

-------------------------------------------------------------------------------

CfP: Math Information Retrieval Worksohp 14. July 2012

2012-03-29T16:34:10

[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&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&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.

mizar parsing/text transformation service

Jesse Alama — 2012-03-20T10:30:07

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

tooltips

Josef Urban — 2012-03-20T02:20:08

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&FormulaURL=http://mizar.cs.ualberta.ca/~mptp/mml4.181.1147/mml/card_1.miz&MMLVersion=4.181.1147&Name=Tst1&GenATP=1&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

Re: Lm9 of xcmplx_1

Jesse Alama — 2012-03-18T20:33:53

Hi Adam,

Thanks; that's exactly what I'm looking for.

The next question is why the same theorem appears twice in the same
article, one time as an unexported lemma and then later as a proper
(exported) theorem.  Once I saw Lm9, I didn't search any further in
the article on the assumption that it wouldn't literally reappear
later.

Jesse

Adam Naumowicz <adamn< at >math.uwb.edu.pl> writes:

Re: Re: Lm9 of xcmplx_1

Adam Naumowicz — 2012-03-18T20:23:17

Jesse,

Look here:

theorem :: XCMPLX_1:89
for b, a being complex number st b <> 0 holds
a = (a * b) / b by Lm9;

Best,

Adam

On Sun, 18 Mar 2012, Jesse Alama wrote:

Re: Lm9 of xcmplx_1

Jesse Alama — 2012-03-18T19:35:27

Hi Andrzej,

At

  http://www.mizar.org/version/current/html/xcmplx_1.html#E62

you can see that the theorem I have in mind is called Lm9 and it is
unexported.  I see this also in the .miz file for the official release
of MML 4.181.1147.  Do you see this as well?  In xreal_1.abs I see

:: [ xreal_1.abs ] ::::::::::::::::::::::::::::::::::::::::::::::::::::

:: snip

theorem :: XCMPLX_1:53 :: REAL_2'31
  c <> 0 & a / c = b / c implies a = b;

theorem :: XCMPLX_1:54 :: REAL_2'74
  a / b <> 0 implies b = a / (a / b);

:: snip

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

with no such lemma (as expected, since it is not exported).

Jesse

trybulec< at >math.uwb.edu.pl writes:

Re: Lm9 of xcmplx_1

2012-03-18T15:52:05

Is it Lm9? I have

Lm9: b<>0 implies a=a*b/b

and it seems that it is so for long time.

Anyway, you need the theorem

theorem :: XCMPLX_1:52  a <> 0 implies a / (a / b) = b;

Maybe in version that you use it has a different number.

Lemmas are often proved because the order in which we prove and the 
order in which we
want to list theorems in abstract are different. Then they are repeated 
as theorems with the justification "by lemma".

I have checked lemmas in XCMPLX_1. All are exported as theorems:

theorem :: REAL_1'24
  a" * b" = (a * b)" by Lm1;
theorem :: REAL_1'42
  a / (b / c) = (a * c) / b by Lm2;
theorem :: REAL_1'43
  b <> 0 implies a / b * b = a by Lm3;
theorem :: REAL_1'33_1
  1 / a = a" by Lm4;
theorem :: REAL_1'37
  a <> 0 implies a / a = 1 by Lm5;
theorem :: REAL_1'35
  (a / b) * (c / d) = (a * c) / (b * d) by Lm6;
theorem :: REAL_1'81
  (a / b)" = b / a by Lm7;
theorem :: SQUARE_1'18
  a * (b / c) = (a * b) / c by Lm8;
theorem :: REAL_2'62_2
  b <> 0 implies a = a * b / b by Lm9;
theorem :: REAL_1'38
  c <> 0 implies a / b = (a * c) / (b * c) by Lm10;
theorem :: REAL_2'47_1
   (a * b")" = a" * b by Lm11;
theorem :: REAL_2'33_1
  a" = b" implies a = b by Lm12;
theorem :: REAL_1'82
  (a / b) / (c / d) = (a * d) / (b * c) by Lm13;
theorem :: REAL_2'56:
  a * (1 / b) = a / b by Lm14;
theorem :: REAL_2'67_4
  1 / c * (a / b) = a / (b * c) by Lm15;
theorem :: REAL_1'33_2
  1 / a" = a by Lm16;
theorem :: REAL_1'39_1
  -a / b = (-a) / b by Lm17;
theorem :: REAL_2'46_1
  a <> 0 & a = a" implies a = 1 or a = -1 by Lm18;
theorem :: REAL_2'45_1
  (- a)" = -a" by Lm19;

Greetings,
Andrzej


Cytowanie Jesse Alama <jesse.alama< at >gmail.com>:

Lm9 of xcmplx_1

Jesse Alama — 2012-03-16T12:39:22

Please promote Lm9 of XCMPLX_1 (MML 4.181.1147)

for a, b being complex number
  st a <> 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

Re: New Mizar articles

Josef Urban — 2012-03-16T10:11:31

Dear All,

the Mizar remote verification/solving/presentation services at
http://mws.cs.ru.nl/~mptp/MizAR.html and
http://mizar.cs.ualberta.ca/~mptp/MizAR.html have now been updated to
include the latest MML version 4.181.1147. I also added to Emacs a
function (mizar-atp-review-proofs) for ATP-based article reviewing
that calls ATPs to justify all toplevel < at >proofs independently (with
the whole MML). Sometimes such proofs are simpler.

Best,
Josef Urban

On Wed, Feb 22, 2012 at 9:13 AM, Adam Grabowski <adam< at >math.uwb.edu.pl> wrote:

vernacular

Josef Urban — 2012-03-15T20:47:37

Here are frequencies (>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

Re: Re: Urelements?

Josef Urban — 2012-03-14T17:48:21

2012/3/14  <trybulec< at >math.uwb.edu.pl>:

Yes.


Yes. (Or: in most cases. I can imagine an ugly theory of cyclic groups.)

So the context for the coercion needs to be specified. Using "element"
in the constructor declaration is indeed one way how to do it. But I
am not sure where it will lead. I'd perhaps prefer to deal with
syntactic problems by purely syntactic mechanisms.


Prove it via extensionality :-).


I wonder what T1 c= T2 typically means for topological spaces. Or for
structures with more carriers.


I think there is a general problem. Structures are an experiment in
marrying abstract/axiomatic approach with concrete set theory. If we
ever specify them extensionally, the "elements" will disappear, and
the right parsing will become even more context-dependent. And already
now the "element" introduction does not solve some of the above
issues.

Best,
Josef

Re: Re: Urelements?

2012-03-14T15:19:36

Cytowanie Josef Urban <josef.urban< at >gmail.com>:


So, by "takes a structural argument" you mean that the type of locus is 
structural, do you? But then, if we write

      G in X
(G - a group) it would be coerced to

      the carrier of G in X,

But if G is a family of groups, and we write

           G in X
we mean exactly what it means without any coercion.

x = y

is not coerced at all, G1 = G2 means that the group are equal

x c= y

both arguments are coreced, G1 c= G2 means     the carrier of G1 c= the 
carrier of G2

For the membership only the second argument is coerced. There are still 
some minor problems e.g. how to cope with the redefinition of the 
equality for sets

     redefine pred A = B means A c= B & B c= A

Regards,
Andrzej

Re: Re: Urelements?

Josef Urban — 2012-03-14T13:45:51

2012/3/14  <trybulec< at >math.uwb.edu.pl>:

No, there is no structural argument in that definition.

Josef

Re: Re: Urelements?

2012-03-14T11:11:06

Cytowanie Josef Urban <josef.urban< at >gmail.com>:



It does not matter that it is a new mechanism. It still does not work.

Let be more precise: what yopu want to do with membership:

          let x,X be set;
          pred x in X;

The membership takes structural arguments, so what Mizar is supposed to do?

Andrzej