Překlad Mizaru pro dokazovače v logice 1. řádu
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F03%3A00005574" target="_blank" >RIV/00216208:11320/03:00005574 - 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
Translating Mizar for first order theorem provers
Popis výsledku v původním jazyce
The constructor system of the Mizar proof checking system is explained here on examples from Mizar articles, and its translation to untyped first-order syntax is described and discussed. This makes the currently largest library of formalized mathematicsavailable to first-order theorem provers.
Název v anglickém jazyce
Translating Mizar for first order theorem provers
Popis výsledku anglicky
The constructor system of the Mizar proof checking system is explained here on examples from Mizar articles, and its translation to untyped first-order syntax is described and discussed. This makes the currently largest library of formalized mathematicsavailable to first-order theorem provers.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
BA - Obecná matematika
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2003
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 periodika
Lecture Notes In Computer Science
ISSN
0302-9743
e-ISSN
—
Svazek periodika
2594
Číslo periodika v rámci svazku
neuveden
Stát vydavatele periodika
DE - Spolková republika Německo
Počet stran výsledku
13
Strana od-do
203-215
Kód UT WoS článku
—
EID výsledku v databázi Scopus
—