Mizar Problems for Theorem Proving (MpTP)

see MpTP02 for second version of MpTP and MptpTodo for suggested improvements
MpTP is collection of theorem proving problems generated automatically from MML
the latest distribution is at http://ktilinux.ms.mff.cuni.cz/~urban/MPTP/MPTP.tar.gz and the basic files for db generation are at http://ktilinux.ms.mff.cuni.cz/~urban/MPTP/MPTPbasic.tar.gz
some documentation is included in the distro, additionally, an article about it is at http://link.springer.de/link/service/series/0558/papers/2594/25940203.pdf and slides at http://monet.nag.co.uk/mkm/bertinoro03/urban.pdf . A more detailed article is now available at http://ktiml.mff.cuni.cz/~urban/MPTP/mptp-jar.ps.gz
current version is 0.1
a very experimental SQL server containing results of provers run on MpTP and some additional info on problems is browsable at http://lipa.ms.mff.cuni.cz/phpMyAdmin-2.4.0/, let me know if you want to submit your own results into it
the SQL structure of the server is described in the atteched file MPTPResults.sql
note that both MpTP and the results server will probably change a lot in the beginning

-- JosefUrban - 07 Jul 2004

I	Attachment	Action	Size	Date	Who	Comment
	MPTPResults.sql	manage	5.3 K	19 Mar 2003 - 23:46	WikiRoot

Edit | Attach image or document | Printable version | Raw text | More topic actions
Revisions: | r1.4 | > | r1.3 | > | r1.2 | Total page history | Backlinks

You are here: Mizar > MpTP

to top