- Referenced in 44 articles
- 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...
- Referenced in 43 articles
- more difficult (chainy) division of the MPTP Challenge solving 142 problems...
- Referenced in 23 articles
- 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...
- Referenced in 20 articles
- initial implementation is evaluated on the MPTP Challenge large theory benchmark...
- Referenced in 17 articles
- MizarMode -- an integrated proof assistance tool for the...
- Referenced in 313 articles
- Our current automated deduction system Otter is designed...
- Referenced in 237 articles
- Vampire 8.0, [RV02,Vor05] is an automatic theorem...
- Referenced in 177 articles
- SPASS is an automated theorem prover for first...
- Referenced in 376 articles
- The TPTP (Thousands of Problems for Theorem Provers...
- Referenced in 32 articles
- MoMM (in the narrower sense) is a tool...
- Referenced in 456 articles
- The Mizar System is the only implementation of...
- Referenced in 47 articles
- Licensing the Mizar Mathematical Library (MML). The Mizar...