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 su

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

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 f

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

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 aspe

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:
Micha

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

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), i

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

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