Reconstruction of the Mizar Type System in the HOL Light System

Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Reconstruction of the Mizar Type System in the HOL Light System
Original language description
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
Czech name
—
Czech description
—

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

Article name in the collection
WDS'10 Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences
ISBN
978-80-7378-139-2
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
—
Publisher name
MATFYZPRESS
Place of publication
Praha
Event location
Praha
Event date
Jun 1, 2010
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
—

Similar results(10)