Není kalkul jako kalkul:

Důkazový systém HOL a logika

Mgr. Jiří RACLAVSKÝ, Ph.D.
Katedra filosofie FF-MU v Brně
raclavsk@phil.muni.cz



Abstrakt

Nejprve se budeme věnovat vůbec tomu, co důkazové systémy (proof assistants, theorem provers) jsou. Největší objem jejich aplikací není v logice, ale v matematice. Záhy se přesuneme k vývojové rodině renomovaných systémů nyní známých jako HOL. Od popisu obecné stavby takového systému se přesuneme k popisu fungování programu při praktickém užití někým, kdo chce něco dokazovat. HOL je zkratka za higher-order logic. Touto logikou je ovšem specifická varianta Churchova typovaného lambda kalkulu (TLK). Nejprve si uvedeme TLK a to na pozadí zobecnění podaném P. Tichým (neplést si s TILem!). Tím upozadíme v HOL neimplementované Churchovy matematické teorie; také nám to umožní srovnání s kalkulem konstrukcí (Coquand). Přesuneme se ke svízelné problematice typové polymorfie a explicitního typování. Postupy zcela nemyslitelné či kacířské v rámci (filosofické) logiky jsou totiž inherentní součástí jazyka HOL. Závěrem se přesuneme k dedukčnímu systému HOL, srovnáme ho např. s Churchovým a Tichého systémem. Následně se ozřejmí, jak si má uživatel dedukční systém rozpracovávat, což je nezbytné k praktickému dokazování. Vybraná literatura: The HOL documentation, http://hol.sourceforge.net/documentation.html Church, Alonzo (1940): A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5: 56-68. Church, Alonzo (1941): The Calculi of Lambda Conversion. Princeton University Press. Andrews, Peter B. (1986): An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press. Tichý, Pavel (1982): The Foundations of Partial Type Theory. Reports on Mathematical

Prezentace

Článek ve sborníku