Reconstruction of the Mizar Type System in the HOL Light System
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F10%3A10081315" target="_blank" >RIV/00216208:11320/10:10081315 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Reconstruction of the Mizar Type System in the HOL Light System
Popis výsledku v původním jazyce
The Mizar system is a system for formalization of mathematics. It contains a relatively sophisticated and rich type system, which makes formalization of mathematics in Mizar more intuitive than in other systems. On the other hand, the Mizar type system is very complex and together with obscure implementation of the Mizar verifier there is concern about correctness of the Mizar system. One of the possible solutions is to translate the Mizar Math Library (MML) to other systems for formalization of mathematics and reverify MML in them. The HOL Light system has been chosen and the necessary first step of proposed translation is to reconstruct the Mizar type system in the HOL Light system, which is the aim of the presented work. The reconstruction is not easy because of complexity of the Mizar type system and different types of logic used in both systems. The basic idea is to represent Mizar types as predicates and express the dynamic part of the Mizar type system as proved theorems in HOL
Název v anglickém jazyce
Reconstruction of the Mizar Type System in the HOL Light System
Popis výsledku anglicky
The Mizar system is a system for formalization of mathematics. It contains a relatively sophisticated and rich type system, which makes formalization of mathematics in Mizar more intuitive than in other systems. On the other hand, the Mizar type system is very complex and together with obscure implementation of the Mizar verifier there is concern about correctness of the Mizar system. One of the possible solutions is to translate the Mizar Math Library (MML) to other systems for formalization of mathematics and reverify MML in them. The HOL Light system has been chosen and the necessary first step of proposed translation is to reconstruct the Mizar type system in the HOL Light system, which is the aim of the presented work. The reconstruction is not easy because of complexity of the Mizar type system and different types of logic used in both systems. The basic idea is to represent Mizar types as predicates and express the dynamic part of the Mizar type system as proved theorems in HOL
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2010
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
WDS'10 Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences
ISBN
978-80-7378-139-2
ISSN
—
e-ISSN
—
Počet stran výsledku
6
Strana od-do
—
Název nakladatele
MATFYZPRESS
Místo vydání
Praha
Místo konání akce
Praha
Datum konání akce
1. 6. 2010
Typ akce podle státní příslušnosti
EUR - Evropská akce
Kód UT WoS článku
—