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

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi,

I suggest, following Jesse's suggestion that the entire .bib files for
Mizar articles be incorporated into the .miz files.

Cheers, PR

On Wed, Nov 19, 2008 at 01:12:34PM -0800, Jesse Alama wrote:
> 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)

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr