Důkazový asistent HOL a jeho logika

RACLAVSKÝ, Jiří. Důkazový asistent HOL a jeho logika. In Organon VIII. Calculemus. Plzeň: Vydavatelství Západočeské univerzity v Plzni, 2012, s. 83-91. ISBN 978-80-261-0145-1.

Základní údaje

• Originální název: Důkazový asistent HOL a jeho logika
• Název česky: Důkazový asistent HOL a jeho logika
• Název anglicky: Proof Assistant HOL and Its Logic
• Autoři: RACLAVSKÝ, Jiří (203 Česká republika, garant, domácí).
• Vydání: Plzeň, Organon VIII. Calculemus, od s. 83-91, 9 s. 2012.
• Nakladatel: Vydavatelství Západočeské univerzity v Plzni

Další údaje

• Originální jazyk: čeština
• Typ výsledku: Stať ve sborníku
• Obor: 60300 6.3 Philosophy, Ethics and Religion
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Kód RIV: RIV/00216224:14210/12:00059614
• Organizační jednotka: Filozofická fakulta
• ISBN: 978-80-261-0145-1
• Klíčová slova anglicky: assistants; theorem provers; HOL; typed lambda-calculus
• Štítky: rivok
• Příznaky: Recenzováno

Anotace

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.

Anotace 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.

Návaznosti

• MUNI/A/0934/2009, interní kód MU: Název: Filozofie: minulé doby, současné problémy

Investor: Masarykova univerzita, Filozofie: minulé doby, současné problémy, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty