Důkazový asistent HOL a jeho logika

Autoři

RACLAVSKÝ Jiří

Rok publikování 2012
Druh Článek ve sborníku
Konference Organon VIII. Calculemus
Fakulta / Pracoviště MU

Filozofická fakulta

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.