request for review: text/mizar

Paul Libbrecht paul at hoplahup.net
Thu Jun 30 15:27:41 CEST 2011


Hello Jesse,
(;-))

a few quick comments but I am sure others will have some more.

- I think you should refer to the RFC template you use, please see the mailing list archive
- I think the change controller should be the association of Mizar users', as an institution with an address, and not the  name of a person; an email can complement it for sure!
- type and subtypes are commonly lowercase... why not continue so?
- 8bit... is there a charset there?
- can the specification be indicated with a publicly accessible URL?
- and finally the personal suggestion: I know Mizar is intended to be manipulated by text editors. Could you add two lines in the additional information that say something such as:
    - Window clipboard flavor: "Mizar"
    - Macintosh Uniform Type Identifier: "org.mizar" conforms to "public.text"
  this way applications can offer fragments in multiple formats on the clipboard, one of them, say, being RTF and the other Mizar, for different objectives.

paul

Le 30 juin 2011 à 14:02, Jesse Alama a écrit :

> Name : Jesse Alama
> 
> Email : j.alama at fct.unl.pt
> 
> MIME media type name : Text
> 
> MIME subtype name : Standards Tree -mizar
> 
> Required parameters : none
> 
> Optional parameters :
> none
> 
> Encoding considerations : 8bit
> 
> 
> Security considerations :
> none
> 
> Interoperability considerations :
> 
> 
> Published specification :
> A. Grabowski, A. Kornilowicz, and A. Naumowicz, "Mizar in a Nutshell",
> Journal of Formalized Reasoning 3(2), 2010, pp. 153--245.
> 
> Applications which use this media :
> The mizar suite of tools
> 
> Additional information :
> 
> 1. Magic number(s) : none
> 2. File extension(s) : .miz
> 3. Macintosh file type code : none
> 4. Object Identifiers: none
> 
> The mizar language is a language for formalized mathematical documents.
> Authors use this langauge to express definitions of mathematical
> concepts, and express and proof formal mathematical statements. The
> language has been developed since the 1970s and today is used in
> teaching logic and mathematics in various high school and universty
> settings. The library of mathematical knowledge formalized in the mizar
> language, the Mizar Mathematical Library, consists (at the time of
> application) of more than 1100 "articles" which, like an ordinary
> mathematical article in a journal, are coherent presentations and
> developments of mathematics.
> 
> Person to contact for further information :
> 
> 1. Name : Jesse Alama
> 2. Email : j.alama at fct.unl.pt
> 
> Intended usage : Common
> This media type is intended to be used by text editors and affiliated
> programs that read text (e.g., web browsers).
> 
> Author/Change controller : Adam Naumowicz
> Association of Mizar Users
> sum at mizar.uwb.edu.pl
> 
> -- 
> Jesse Alama
> http://centria.di.fct.unl.pt/~alama/
> 
> 



More information about the Ietf-types mailing list