Důkazový asistent HOL a jeho logika

Title in English Proof assistant HOL and its logic


Type Conference abstract
MU Faculty or unit

Faculty of Arts

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: