Důkazový asistent HOL a jeho logika

Varování

Publikace nespadá pod Fakultu sociálních studií, ale pod Filozofickou fakultu. Oficiální stránka publikace je na webu muni.cz.

Autoři	RACLAVSKÝ Jiří
Rok publikování	2012
Druh	Článek ve sborníku
Konference	Organon VIII. Calculemus
Fakulta / Pracoviště MU	Filozofická fakulta
Citace
Obor	Filosofie a náboženství
Klíčová slova	assistants; theorem provers; HOL; typed lambda-calculus
Popis	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.
Související projekty:	Filozofie: minulé doby, současné problémy