- Referenced in 42 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 40 articles
- more difficult (chainy) division of the MPTP Challenge solving 142 problems...
- Referenced in 21 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 18 articles
- initial implementation is evaluated on the MPTP Challenge large theory benchmark...
- Referenced in 15 articles
- MizarMode -- an integrated proof assistance tool for the...
- Referenced in 290 articles
- Our current automated deduction system Otter is designed...
- Referenced in 203 articles
- Vampire 8.0, [RV02,Vor05] is an automatic theorem...
- Referenced in 154 articles
- SPASS is an automated theorem prover for first...
- Referenced in 333 articles
- The TPTP (Thousands of Problems for Theorem Provers...
- Referenced in 31 articles
- MoMM (in the narrower sense) is a tool...
- Referenced in 387 articles
- The Mizar System is the only implementation of...
- Referenced in 46 articles
- Licensing the Mizar Mathematical Library (MML). The Mizar...