
MPTP 0.2
 Referenced in 44 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 43 articles
[sw10278]
 more difficult (chainy) division of the MPTP Challenge solving 142 problems...

MPTP
 Referenced in 23 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 20 articles
[sw07197]
 initial implementation is evaluated on the MPTP Challenge large theory benchmark...

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

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

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

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

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

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

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

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