[mizar] an extension of the mizar language for dealing with article metadata

[Jesse Alama <alama@stanford.edu>]

As it stands now, the title of an article, its author(s), and the name
of sections aren't actually a formal part of a mizar text: we
customarily include this information as comments

  :: Introduction to XYZ Theory
  ::
  :: by Joe the MIZAR Writer

  environ

  ...

  begin :: Preliminaries

  ...

  begin :: Main Lemma

  ...

  begin :: Main Theorem

  ...

I propose to put this information into the body of the article, to move
it from comments to non-comments.  Perhaps we could introduce new
keywords like `title', `author', and `section'.  Then, articles could
look like

 title{Introduction to XYZ Theory}
 author{Joe the MIZAR Writer}

 environ

   <stuff>

 begin{Preliminaries}

 definition ...

 theorem ...

 theorem ...

 begin{Main Lemma}

 definition ...

 begin{Main Theorem}

 theorem ...

This would make the sections and article title part of the text; as it
stands, these features are not represented in the mizar grammar (because
customarily they are tucked away within comments).

The primary motivation for this idea is to help improve Josef Urban's
semantic MML presentation.  Currently he has to do some hacking to
extract metadata like article titles and authors; extracting section
information (currently unsupported) would be similarly complicated.  The
problem is that the article metadata isn't represented in the XML
representation of an article; it has to be inferred from the original
mizar source.

Additionally, this new syntax might help to simplify processing of FM
articles: with this approach one wouldn't need the BibTeX fields
SECTION1, SECTION2, etc., because these could be inferred from the
article.

Thoughts?

Best,

Jesse

-- 
Jesse Alama (alama@stanford.edu)