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%3A00059614" target="_blank" >RIV/00216224:14210/12:00059614 - 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

Tento článek 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 paper, 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

D - Stať ve sborníku

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ů

Název statě ve sborníku

Organon VIII. Calculemus

ISBN

9788026101451

ISSN

—

e-ISSN

—

Počet stran výsledku

9

Strana od-do

83-91

Název nakladatele

Vydavatelství Západočeské univerzity v Plzni

Místo vydání

Plzeň

Místo konání akce

Telč

Datum konání akce

1. 1. 2012

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

EUR - Evropská akce

Kód UT WoS článku

—