ATP Cross-Verification of the Mizar MPTP Challenge Problems
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F07%3A00206156" target="_blank" >RIV/00216208:11320/07:00206156 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
ATP Cross-Verification of the Mizar MPTP Challenge Problems
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
—
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Logic for Programming, Artificial Intelligence, and Reasoning
ISBN
978-3-540-75558-6
ISSN
—
e-ISSN
—
Number of pages
15
Pages from-to
—
Publisher name
Springer
Place of publication
Berlin
Event location
Berlin
Event date
Jan 1, 2007
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000251785100039