ATP Cross-Verification of the
Mizar MPTP Challenge Problems

Introduction

• What is Mizar?
• The MPTP Challenge
• Why ATP for Mizar?

Translation of MML Proofs to TPTP Derivations

• Mizar justifications
  • Simple Mizar Proofs
  • Mizar Proof involving Quantifiers
  • Mizar Proof Structure
  • Simplified grammar of Mizar justifications
• TPTP derivations and verification
  • TPTP Syntax for Assumptions
  • Verification with GDV
• Translation of Mizar Assumption/Conclusion rules to TPTP
• Translation of Mizar Let rule to TPTP

Verification of the MPTP Challenge problems

• GDV Pass
• MaLARea Pass
• Human Pass

Conclusion