La théorie des types et les systèmes informatiques de traitement de démonstrations mathématiques

Mathématiques et sciences humaines. Mathematics and social sciences

Dowek, Gilles¹ 

关键词: type theory;    set theory;    proof;    deduction;    computation;    mathematical language;    function;    proof processing systems;   

DOI  :  10.4000/msh.2904

学科分类：数学（综合）

来源: College de France * Ecole des Hautes Etudes en Sciences Sociales (E H E S S)

【 摘 要 】

Since the end of the sixties, several computer programs allowing to process mathematical knowledge, and in particular mathematical proofs, have been designed. Building such programs raises new questions, in particular that of the conception of logical frameworks where mathematics can be formalized in practice. This is a new direction for fundational studies, more interested, so far, in formalization of mathematics in principle, than in practice. Several reasons explain that the designers of such programs often chose type theory rather than set theory to formalize mathematics.

【 授权许可】

Unknown