Accueil Dernière Parution Auteurs Thèmes Mots-clefs Parutions Videos Recherche guidée Comité de lecture Contact Abonnement Soumission d'article   Version anglaise Collection numérisée également sur NUMDAM pour les n°1 à n°148 et sur Revues.org pour les n° 149 et suivants

Recherche selon le critère: Mot-clef: Raisonnement Affiner ou élargir la recherche 1 entrée référencée Titre La théorie des types et les systèmes informatiques de traitement de démonstrations mathématiques Auteur DOWEK Gilles Mots-clefs Calcul, Démonstration, Fonction, Langage mathématique, Raisonnement, Systèmes de traitement de démonstrations mathématiques, Théorie des ensembles, Théorie des types Thèmes Calcul, Ensembles (Théorie des), Informatique, Logiciel, Logique 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. Numéro 165, Printemps 2004, n° spécial La théorie constructive des types Langue   Français Lire l'article Droits des utilisateurs : Cette création est mise à disposition sous un contrat Creative Commons