MPTP Challenge: Why, What, How, Results, What to do Next

Current TPTP, CASC, ATP

TPTP in 2003:

• mostly CNF problems

• ATPs working mostly in CNF, only a few exceptions (Flotter/SPASS, Otter's clausifier)

• problems in TPTP not related to each other (as a rule)

• specialized problem solving methods for classes of problems beginning, tuning done before CASC

Intentions

• motivate ATP research in large theories
• move tuning of ATPs to execution time
• well-defined benchmark for systems working in LT
• evaluate/show potential of new methods not used so far in ATP

Related Large Theory efforts:

• 1992: Art Quaife: Automated Development of Fundamental Mathematical Theories (Freeze a jolly good fellow!) using Otter to develop Set Theory and other fields very often CNF

• 2004-2006: Larry Paulson & Jia Meng: ATP problems from Isabelle

• 2005-2007: Pace Reagan-Smith: Translation of CyC? to TPTP (work in progress), Using SPASS on CyC?

• 2002-2007: Adam Pease, Andrei Voronkov: Using Vampire on SUO-KIF Ontologies (SUMO, etc.). translation of SUO-KIF to TPTP (work in progress)

Related ATP efforts for large theories

• 2004-6: Isabelle: pruning of the axiom set using symbol-based heuristics
• 2006: EPROVER - ConjectureWeight? based on symbols in the conjecture
• 2003: Vampire-SUMO, SOS-mode,

Other pressures at ATPs

• decision procedures - SPASS+T (added theory solver - Yices, CVCLite - only integers now),

• SMT (Satisfiability Modulo Theory) - Yices, CVCLite, etc.

How

• select a suitable subDAG from MPTP, practically created the following Prolog data from Mizar:

th_rec_uses(Theorem,Nonnumerical,LengthAllRec,LengthAllRecNN,AllChainLength, AllNNChainLength?,LargestParent,LargestParentNN,LongestParent, LongestParentNN?,AllRecUses,AllRecNonNumUses)

• should be a nontrivial mathematical theorem
• a large theory should be really needed, or at least natural (not just axioms of a group)
• should minimize numerical evaluations
• the leaves should be MML definitions and axioms

Candidates and problems

• giving the Mizar symbols sensible names (about 600 TPTP-compatible symbol names done): http://wiki.mizar.org/cgi-bin/twiki/view/Mizar/NiceConstructorNames
• good subDAGs with bad theorems
• handling of second-order Mizar features not perfect in the first version
• one implication of Bolzano-Weierstrass theorem finally chosen

Divisions

• bushy - easier
• chainy - more AI

Statistics

• MML: MML (as of July 2006) contains 942 formal articles (with 42694 theorems, and 7957 definitions) from various fields of mathematics.
• 252 problems in each division

Results

• LeanCop? - surprisingly good
• two metasystems so far

-- JosefUrban - 20 Nov 2007