Důkazový asistent HOL a jeho logika

Title in English Proof Assistant HOL and Its Logic


Type Article in Proceedings
Conference Organon VIII. Calculemus
MU Faculty or unit

Faculty of Arts

Field Philosophy and religion
Keywords assistants; theorem provers; HOL; typed lambda-calculus
Description 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.
Related projects: