ATP cross-verification of the mizar MPTP challenge problems

Josef Urban; Geoff Sutcliffe

doi:10.1007/978-3-540-75560-9_39

ATP cross-verification of the mizar MPTP challenge problems

Josef Urban, Geoff Sutcliffe

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Scopus citations

Abstract

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 by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system), ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.

Original language	English (US)
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings
Publisher	Springer Verlag
Pages	546-560
Number of pages	15
ISBN (Print)	9783540755586
DOIs	https://doi.org/10.1007/978-3-540-75560-9_39
State	Published - 2007
Event	14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007 - Yerevan, Armenia Duration: Oct 15 2007 → Oct 19 2007

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4790 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007
Country	Armenia
City	Yerevan
Period	10/15/07 → 10/19/07

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-75560-9_39

Fingerprint Dive into the research topics of 'ATP cross-verification of the mizar MPTP challenge problems'. Together they form a unique fingerprint.

Cite this

Urban, J., & Sutcliffe, G. (2007). ATP cross-verification of the mizar MPTP challenge problems. In Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings (pp. 546-560). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4790 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-540-75560-9_39

ATP cross-verification of the mizar MPTP challenge problems. / Urban, Josef; Sutcliffe, Geoff.

Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings. Springer Verlag, 2007. p. 546-560 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4790 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Urban, J & Sutcliffe, G 2007, ATP cross-verification of the mizar MPTP challenge problems. in Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4790 LNAI, Springer Verlag, pp. 546-560, 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007, Yerevan, Armenia, 10/15/07. https://doi.org/10.1007/978-3-540-75560-9_39

Urban J, Sutcliffe G. ATP cross-verification of the mizar MPTP challenge problems. In Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings. Springer Verlag. 2007. p. 546-560. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-75560-9_39

Urban, Josef ; Sutcliffe, Geoff. / ATP cross-verification of the mizar MPTP challenge problems. Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings. Springer Verlag, 2007. pp. 546-560 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e9c23f5f88e64a838f362466eb015434,

title = "ATP cross-verification of the mizar MPTP challenge problems",

abstract = "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 by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system), ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.",

author = "Josef Urban and Geoff Sutcliffe",

year = "2007",

doi = "10.1007/978-3-540-75560-9_39",

language = "English (US)",

isbn = "9783540755586",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "546--560",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings",

note = "14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007 ; Conference date: 15-10-2007 Through 19-10-2007",

}

TY - GEN

T1 - ATP cross-verification of the mizar MPTP challenge problems

AU - Urban, Josef

AU - Sutcliffe, Geoff

PY - 2007

Y1 - 2007

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 by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system), ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.

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 by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system), ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.

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

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

U2 - 10.1007/978-3-540-75560-9_39

DO - 10.1007/978-3-540-75560-9_39

M3 - Conference contribution

AN - SCOPUS:38149064402

SN - 9783540755586

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 546

EP - 560

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings

PB - Springer Verlag

T2 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007

Y2 - 15 October 2007 through 19 October 2007

ER -