ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments |
| |
Authors: | Josef Urban Geoff Sutcliffe |
| |
Institution: | (1) Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics, Charles University, Malostranske namesti 2/25, 118 00 Praha 1, Czech Republic;(2) Department of Computer Science, University of Miami, P.O. Box 248154, Coral Gables, FL 33124-4245, USA |
| |
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 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.
Supported by a Marie Curie International Fellowship within the 6th European Community Framework Programme. |
| |
Keywords: | Mathematics Subject Classification (2000)" target="_blank">Mathematics Subject Classification (2000) Primary 03E99 Secondary 68T15 |
本文献已被 SpringerLink 等数据库收录! |
|