ATP cross-verification of the mizar MPTP challenge problems

Josef Urban, Geoffrey Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages546-560
Number of pages15
Volume4790 LNAI
StatePublished - 2007
Event14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007 - Yerevan, Armenia
Duration: Oct 15 2007Oct 19 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4790 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007
CountryArmenia
CityYerevan
Period10/15/0710/19/07

Fingerprint

Automated Theorem Proving
Theorem proving
1-Methyl-4-phenyl-1,2,3,6-tetrahydropyridine
Libraries
Mathematics
Formalization
Correctness
Verify

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Urban, J., & Sutcliffe, G. (2007). ATP cross-verification of the mizar MPTP challenge problems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4790 LNAI, pp. 546-560). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4790 LNAI).

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 proceedingConference contribution

Urban, J & Sutcliffe, G 2007, ATP cross-verification of the mizar MPTP challenge problems. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 4790 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4790 LNAI, pp. 546-560, 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007, Yerevan, Armenia, 10/15/07.
Urban J, Sutcliffe G. ATP cross-verification of the mizar MPTP challenge problems. In 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)).
Urban, Josef ; Sutcliffe, Geoffrey. / ATP cross-verification of the mizar MPTP challenge problems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4790 LNAI 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 Geoffrey Sutcliffe",
year = "2007",
language = "English (US)",
isbn = "9783540755586",
volume = "4790 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "546--560",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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 -