Mathématiques et sciences humaines/Mathematics and social sciences

n° 165, Printemps 2004, spécial La théorie constructive des types

Version imprimable   Signaler cette page  

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

Type theory and proof processing system

Gilles Dowek

Télécharger le texte intégral (225k)

Résumé

Depuis la fin des années soixante, on a vu apparaître plusieurs logiciels destinés à traiter des connaissances mathématiques, en particulier des démonstrations formelles. La réalisation de tels logiciels pose de nouveaux problèmes, en particulier celui de la conception de cadres logiques dans lesquels les mathématiques puissent être formalisées en fait. Cela renouvelle la problématique des fondements des mathématiques, jusque-là davantage concentrée sur la potentialité de la formalisation que sur son actualité. Plusieurs raisons expliquent que les concepteurs de tels logiciels choisissent bien souvent de formaliser les mathématiques en théorie des types, plutôt qu'en théorie des ensembles.

Abstract

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.

Index

Pour citer cet article

Gilles Dowek, « La théorie des types et les systèmes informatiques de traitement de démonstrations mathématiques », Mathématiques et sciences humaines, n° 165, Printemps 2004, spécial La théorie constructive des types, [En ligne], mis en ligne le 22 février 2006. URL : http://msh.revues.org/document2904.html. Consulté le 28 novembre 2009.

 
Page générée par Lodel - Nous adhérons à www.revues.org

ISSN : 0987 6936
Ecole des hautes études en sciences sociales