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 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 546-560 |
| Number of pages | 15 |
| Volume | 4790 LNAI |
| 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) | 03029743 |
| ISSN (Electronic) | 16113349 |
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 |
Fingerprint
ASJC Scopus subject areas
- Computer Science(all)
- Biochemistry, Genetics and Molecular Biology(all)
- Theoretical Computer Science
Cite this
ATP cross-verification of the mizar MPTP challenge problems. / Urban, Josef; Sutcliffe, Geoffrey.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4790 LNAI 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
}
TY - GEN
T1 - ATP cross-verification of the mizar MPTP challenge problems
AU - Urban, Josef
AU - Sutcliffe, Geoffrey
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
M3 - Conference contribution
SN - 9783540755586
VL - 4790 LNAI
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 546
EP - 560
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -