[mizar] Mizar Problems for Theorem Proving

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Mizar Problems for Theorem Proving (MPTP) version 0.1 
is at http://ktilinux.ms.mff.cuni.cz/~urban/MPTP/MPTP.tar.gz .

The packed full distribution has about 70M and contains databases 
and scripts for generating proving problems from 
1) complete proofs of Mizar theorems (about 30000)
2) Mizar simple justifications - checker problems (about 630000).

If you want to generate the databases from your own Mizar 
distribution, the necessary files only are at 
http://ktilinux.ms.mff.cuni.cz/~urban/MPTP/MPTPbasic.tar.gz
(packed to about 230k). Generation of databases takes about 1 hour
on P4.

Some documentation can be found in the distro, paper and slides about it 
are at
http://link.springer.de/link/service/series/0558/papers/2594/25940203.pdf
and http://monet.nag.co.uk/mkm/bertinoro03/urban.pdf.

Since this is a very early version, I have not set up any server yet for 
browsing and mining results of provers run on the problems and adding 
new results, but I plan some publicly available SQL db for this later.

Josef Urban