Důkazový asistent HOL a jeho logika

Title in English Proof assistant HOL and its logic
Authors

RACLAVSKÝ Jiří

Type Conference abstract
MU Faculty or unit

Faculty of Arts

Citation
Description In the first part of this lecture, 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: