ATP Cross-Verification of the Mizar MPTP Challenge Problems

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

ATP Cross-Verification of the Mizar MPTP Challenge Problems

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

ATP Cross-Verification of the Mizar MPTP Challenge Problems

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Logic for Programming, Artificial Intelligence, and Reasoning

ISBN

978-3-540-75558-6

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Berlin

Datum konání akce

1. 1. 2007

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000251785100039