MizarMML-DB Files

1. MizarMML-DB

The MizarMML-DB, a free open source database for Mizar Aricles, is made use of 
with SQL Server 2008 (Express Edition). It can be customized by SQL Server 
Management Studio or sqlcmd. This database has no inserted initial data. 
The user can freely customize it.

Note that MizarMML-DB.mdf and MizarMML-DB_log.ldf are both to be downloaded 
and they are to be "attached" by SQL Server Management Studio when one uses 
it at first. 

The directory of MizarMML-DB consists of:

1. MizarMML-DB.mdf : MizarMML-DB itself
2. MizarMML-DB_log.ldf : the log file for MizarMML-DB
3. createMLL-DB-Catalogue.sql : the SQL sentence to create MMLCatalogue Table
4. createMML-DB-Category.sql : the SQL sentence to create Category Table
5. createMML-DB.sql : the SQL sentence to create MizarMML-DB
6. readme090927.txt : this file

The directory of download consists of:

1. MakeInsertMML.zip : this contains all the files for MakeInsertMML
2. MizarMML-DB.zip : this contains all the files from the directory of 
MizarMML-DB except for readme090927.txt

(We assume that SQL Server 2008 (Express Edition) is installed in the default 
setting, that is, in C:\Program Files.)

For the specification of the tables, please refer to the above sql-files. 
We use the latest suitable data types as possible for the database. Note that 
this database can not be used with SQL Server 2005 (Express Edition) and the 
older versions because of the new data types.

If one correctly inputs necessary data in the main form of it, it will provide 
a sql-file (InsertMML_(MML Identifier of the Mizar article concerned).sql) 
under the directory C:/mizar/doc.

MizarMML-DB was designed and implemented by Takao Inoue.

///////////////////////////////////////////////////////////////////////////////

2. MakeInsertMML (or Make InsertSQL for MML)

Temporaly, MakeInsertMML (or Make InsertSQL for MML), a GUI Windows utility 
software, is available as a maker of sql-insert-sentences for the 
MizarMML-DB. It is a pre-alpha version, which will be updated. The author 
of MakeInsertMML is Takao Inoue. It was written with Visual C# 2008.

Note that mizar system is to be installed in the default directory, 
that is C:/mizar to use this application correctly. 

///////////////////////////////////////////////////////////////////////////////

<Note>

1. September 27, 2009: I wrote an article titled by "MizarMML-DB, a simple 
free Database for Mizar Articles" which will be submitted for publication in 
"Mechanized Mathematics and Its Applications". Please refer to it for the 
details of the database and the tool, if it will publish.

///////////////////////////////////////////////////////////////////////////////

Copyright (C) 2009 Takao Inoue All Rights Reserved.

EMail: takao_inoue_logic@ybb.ne.jp

The contents of this file were written by Takao Inoue. September 27, 2009