Důkazový asistent HOL a jeho logika

Title in English Proof assistant HOL and its logic


Year of publication 2012
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:

You are running an old browser version. We recommend updating your browser to its latest version.