MPTP 0.2 (Mizar Problems for Theorem Proving)

Installation:
-------------

- If you only want to try proving some problems, unpack 
  problems_nonnumeric.tar.gz or problems_nonnumeric_dfg.tar.gz,
  and try to find a completion with your favourite ATP :-) 
  (if you do, then you have found a bug, please e-mail to 
  urban@kti.mff.cuni.cz).

Otherwise:

- Set the variable mml_dir at the top of utils.pl 
  to the location of the unpacked 'pl' directory in the distro.
- If you want to work with the XML files too, unpack the file
  xml.tar.gz. It will take almost 2GB.
- If you want to browse the html documentation too, unpack the file
  html.tar.gz. It will take almost 600MB.
- The prolog files are tested only with SWI Prolog 5.2 now.
- Load utils.pl into SWI.
- Try generating theorem problems for nonnumerical MML articles by 
  running mk_nonnumeric/0 (about 300 articles and 12500 problems).
- Try generating theorem problems for first 100 MML articles by 
  running mk_first100/0.
- Try running latest EPROVER (www.eprover.org) on the problems
  (the --tstp-in flag is needed).
- Data for machine learning on proofs of MML theorems are
  created by running predicate print_thms_and_defs_for_learning/0.
  It will create file 'Proof_learning' in the current directory,
  with definitions and theorems and their proof references.
- That's it for now. For working with the prolog files 
  study/extend utils.pl for your needs. Or work directly with 
  the rich XML files (directory 'xml').


Files:
------
Proof_learning  ... file with definitions and theorems with their proof 
                    references, usable for Mizar Proof Advisor-like
		    machine learnings 
README          ... this file
constr_names.pl ... SWI-loadable file with pretty-printing symbol names.
                    Load this into SWI and problems will be printed
		    with Mizar-like names. Tested with EProver 0.9 only.
html.tar.gz     ... packed html semantic decsription of articles, 
		    unpacks to 600MB
mizar-7.6.01_4.48.930-i386-linux-mptp.tar.gz ...
		    Custom Mizar distro used for this MPTP. The linux
		    version of 4.48.930 has not been officially released
		    by the time of MPTP0.2 release, so this is made from the 
		    Windows release. The binaries are a newer version
		    (7.6.02), including changes needed for MPTP0.2 and the
		    scheme reporting support compiled in. Chances are
		    that the next official linux release will have all this
		    by default.
mml.lar  	... List of regular Mizar articles in the Mizar distro
problems_nonnumeric.tar.gz     ... packed nonnumeric problems in TPTP syntax
problems_nonnumeric_dfg.tar.gz ... packed nonnumeric problems in DFG syntax
snow_nonnumeric.plres          ... 
			processed results form the incremental AI-assisted
                        ATP (E and SPASS), run on the nonnumerical problems. 
			Can be used for comparison with the original MML
			proofs and various data-mining. The format is:
			proved(Theorem,File,DirectRefs,Background,Info).
xml.tar.gz 	... packed xml directory - takes about 2GB unpacked
utils.pl 	... Prolog utilities for generating ATP problems, etc.


doc/     ... articles about MPTP and Mizar XML.

mizar/   ... the custom Mizar distro used for this MPTP version 
	     unpacks here.

pl/      ... Prolog version of MML, some XML files are not yet 
             translated to Prolog. See doc/mptp2.ps for documentation,
	     and also www.tptp.org for documentation of the TPTP and 
             TSTP formats.

pl/*.the2 .. Theorem files.
pl/*.dco2 .. Constructor files.
pl/*.dcl2 .. Cluster files.
pl/*.evl2 .. Environment files.
pl/*.sch2 .. Scheme files.
pl/*.xml2 .. Files containing all propositions from the articles
             and sort declarations for all local constants in the 
	     articles.


problems/ .. ATP problems generated by utils.pl are placed here.

html/     .. disambiguated browsable form of articles, useful for
	     learning what the theorems and definitions are about;
	     not needed for any problem creation.

utils/	 ... various simple utilities

xml/     ... rich Mizar XML files, not needed if working only in Prolog.
             See doc/mizxml.ps for some documentation, and xmldoc/
	     for corresponding schemes.

xml/*.dco1 .. Constructor files.
xml/*.xml1 .. Complete description of an articles.

xmldoc/  ... documentation of the Mizar XML format

xsl/     ... Directory with XSL scripts for creating MPTP. 
             See doc/mizxml.ps for some documentation.

xsl/addabsrefs.xsl  ... create rich Mizar XML from normal Mizar XML
xsl/mizpl.xsl       ... create Prolog MPTP files from rich Mizar XML
xsl/miz.xsl         ... create the html doc from normal Mizar XML
xsl/constrnames.xsl ... print the mapping to pretty-printing names


License:

GPL