TY - JOUR

T1 - ATP-based cross-verification of Mizar proofs

T2 - Method, systems, and first experiments

AU - Urban, Josef

AU - Sutcliffe, Geoff

N1 - Funding Information:
Supported by a Marie Curie International Fellowship within the 6th Framework Programme.

PY - 2008/12

Y1 - 2008/12

N2 - Mizar is a proof assistant used for formalization and mechanical verification of mathematics. The main use of Mizar is in the development of the Mizar Mathematical Library (MML), in which proofs are verified by the Mizar proof checker. The Mizar proof checker has a quite complex implementation, and also lacks the ability to print out detailed atomic proof steps in a format that is easy to verify with an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes a translation of Mizar natural-deduction proofs to the TPTP format used for recording derivations from first-order automated theorem proving systems, and verification of the resulting TPTP format derivations. The system was tested on two nontrivial sets of Mizar problems: the 252 "MPTP Challenge" problems, and 245 Mizar root theorems. The results of these tests are encouraging, and indicate that cross-verification of the whole MML is feasible.

AB - Mizar is a proof assistant used for formalization and mechanical verification of mathematics. The main use of Mizar is in the development of the Mizar Mathematical Library (MML), in which proofs are verified by the Mizar proof checker. The Mizar proof checker has a quite complex implementation, and also lacks the ability to print out detailed atomic proof steps in a format that is easy to verify with an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes a translation of Mizar natural-deduction proofs to the TPTP format used for recording derivations from first-order automated theorem proving systems, and verification of the resulting TPTP format derivations. The system was tested on two nontrivial sets of Mizar problems: the 252 "MPTP Challenge" problems, and 245 Mizar root theorems. The results of these tests are encouraging, and indicate that cross-verification of the whole MML is feasible.

KW - Automated reasoning

KW - Formalized mathematics

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=69949181682&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=69949181682&partnerID=8YFLogxK

U2 - 10.1007/s11786-008-0053-7

DO - 10.1007/s11786-008-0053-7

M3 - Article

AN - SCOPUS:69949181682

VL - 2

SP - 231

EP - 251

JO - Mathematics in Computer Science

JF - Mathematics in Computer Science

SN - 1661-8270

IS - 2

ER -