You are here:
Publication details
Důkazový asistent HOL a jeho logika
Title in English | Proof assistant HOL and its logic |
---|---|
Authors | |
Year of publication | 2012 |
Type | Conference abstract |
MU Faculty or unit | |
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: |