Mizar Problems for Theorem Proving 0.2 - second version of the MpTP system (MpTP02)

• MpTP02 is downloadable at http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar.gz
• several articles describing MpTP02 are included in the distro, the most recent is also at http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp2.ps
• 2408 new (or rather independent) proofs found by a cooperative run of the MizarProofAdvisor and ATPs on 276 MML articles are at http://kti.ms.mff.cuni.cz/~urban/MPTP2/snow_all.plres
• 329 proofs from above, which are shorter than the MML original can be viewed at http://kti.ms.mff.cuni.cz/~urban/MPTP2/snow_shortened.res
• The MpTPChallenges (http://www.tptp.org/MPTPChallenge/) are sets of classical first-order reasoning problems based on MML and MpTP, expressed in the TpTP language.The winners of each of its two division will be announced at CADE-21, and will each receive $100 in real US dollars.

• MptpTodo is a list of plans and suggestions for future MpTP versions

-- JosefUrban - 23 Oct 2006