
MPTP 0.2
 Referenced in 42 articles
[sw02589]
 MPTP 0.2: Design, implementation, and initial experiments. This paper describes the second version ... Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with ... goal of the MPTP project is to make the large formal Mizar Mathematical Library ... based ATP methods. This version of MPTP switches to a generic extended TPTP syntax that...

MaLARea
 Referenced in 40 articles
[sw10278]
 more difficult (chainy) division of the MPTP Challenge solving 142 problems...

MPTP
 Referenced in 21 articles
[sw02489]
 proceed to describe the implementation of the MPTP system, which makes the largest existing corpus ... formalized mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system ... results of first experiments with reproving the MPTP problems with theorem provers. We also describe ... results of this combined MPA/ATP architecture on MPTP...

MaLeCoP
 Referenced in 18 articles
[sw07197]
 initial implementation is evaluated on the MPTP Challenge large theory benchmark...

MizarMode
 Referenced in 15 articles
[sw01973]
 MizarMode  an integrated proof assistance tool for the...

OTTER
 Referenced in 290 articles
[sw02904]
 Our current automated deduction system Otter is designed...

VAMPIRE
 Referenced in 203 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

SPASS
 Referenced in 154 articles
[sw04108]
 SPASS is an automated theorem prover for first...

TPTP
 Referenced in 333 articles
[sw04143]
 The TPTP (Thousands of Problems for Theorem Provers...

MoMM
 Referenced in 31 articles
[sw04655]
 MoMM (in the narrower sense) is a tool...

Mizar
 Referenced in 387 articles
[sw04704]
 The Mizar System is the only implementation of...

MML
 Referenced in 46 articles
[sw06970]
 Licensing the Mizar Mathematical Library (MML). The Mizar...