Publication details
Důkazový asistent HOL a jeho logika
| Title in English | Proof Assistant HOL and Its Logic |
|---|---|
| Authors | |
| Year of publication | 2012 |
| Type | Article in Proceedings |
| Conference | Organon VIII. Calculemus |
| MU Faculty or unit | |
| Citation | |
| 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: |