Důkazový asistent HOL a jeho logika
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Článek ve sborníku |
| Konference | Organon VIII. Calculemus |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Filosofie a náboženství |
| Klíčová slova | assistants; theorem provers; HOL; typed lambda-calculus |
| Popis | Tento článek 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: |