Důkazový asistent HOL a jeho logika

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F12%3A00059616" target="_blank" >RIV/00216224:14210/12:00059616 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

čeština

Název v původním jazyce

Důkazový asistent HOL a jeho logika

Popis výsledku v původním jazyce

Přednáška má dvě části. V prvé stručně referuji o softwarech nazývaných proof assistants či interactive theorem provers. V druhé části se soustředím na popis logiky, která je zabudována do jednoho z nejznámějších takovýchto softwarů, HOL. Ačkoli HOL je zkratkou za 'higher-order logic', což by snad mohla být jistá predikátová logika, jedná se o lambda kalkul s typy.

Název v anglickém jazyce

Proof assistant HOL and its logic

Popis výsledku anglicky

In the first part of this lecture, I report on actual development of software called proof assistants or interactive theorem provers. In the second part of the paper, I focus on the description of logic inbuilt in one of the most known proof assistants,HOL, which is a kind of typed lambda-calculus.

Druh

O - Ostatní výsledky

CEP obor

AA - Filosofie a náboženství

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

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ů