Důkazový asistent HOL a jeho logika

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

Basic information

• Original name: Důkazový asistent HOL a jeho logika
• Name in Czech: Důkazový asistent HOL a jeho logika
• Name (in English): Proof Assistant HOL and Its Logic
• Authors: RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution).
• Edition: Plzeň, Organon VIII. Calculemus, p. 83-91, 9 pp. 2012.
• Publisher: Vydavatelství Západočeské univerzity v Plzni

Other information

• Original language: Czech
• Type of outcome: Proceedings paper
• Field of Study: 60300 6.3 Philosophy, Ethics and Religion
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• RIV identification code: RIV/00216224:14210/12:00059614
• Organization unit: Faculty of Arts
• ISBN: 978-80-261-0145-1
• Keywords in English: assistants; theorem provers; HOL; typed lambda-calculus
• Tags: rivok
• Tags: Reviewed

Abstract

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.

Abstract (in English)

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.

Links

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

Investor: Masaryk University, Category A