Důkazový asistent HOL a jeho logika
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Konferenční abstrakty |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | Přednáška má dvě části. V prvé stručně referuji o softwarech nazývaných proof assistants či interactive theorem provers. V druhé části se soustředím na popis logiky, která je zabudována do jednoho z nejznámějších takovýchto softwarů, HOL. Ačkoli HOL je zkratkou za 'higher-order logic', což by snad mohla být jistá predikátová logika, jedná se o lambda kalkul s typy. |
| Související projekty: |