Vérité mathématique, cohérence logique et vérification informatique

Show full item record

Files in this item

PDF MURS_2006_49_42.pdf 356.1Kb

Pour citer ce document :
URI: http://hdl.handle.net/2042/15264
Title: Vérité mathématique, cohérence logique et vérification informatique
Author: HUET, Gérard
Abstract: La Mathématique n'est pas une science naturelle, susceptible de vérification expérimentale. La vérité mathématique repose sur une notion de cohérence logique, mais le phénomène d'incomplétude fait qu'on ne peut espérer un fondement mathématique rigoureux intrinsèque. De plus, le développement de très grandes preuves ne permet plus une vérification manuelle. Cette fragilisation de l'édifice mathématique est préoccupante à l'heure où notre tissu industriel, économique, social et médical repose sur l'utilisation de méthodes mathématiques à grande échelle. Le développement de l'Informatique permet néanmoins d'y remédier, notamment par la mise au point de nouvelles notations de preuves (théorie des types) ayant de bonnes propriétés calculatoires et linguistiques. L'augmentation des puissances de calcul disponibles, couplée à l'utilisation d'algorithmes sophistiqués, permet une vérification mécanique des démonstrations les plus touffues, comme en témoigne la nouvelle démonstration du théorème des 4 couleurs, vérifiée grâce à l'assistant de preuves Coq.
Subject: Assistant de preuve; Programme informatique; Démonstration automatique; Théorie des types; Calculabilité; Mathématiques; Logique; Cohérence; Vérité; Informatique; Paradoxe; Démonstration; Logique mathématique; Siècle 20; Proof assistant; Computer programme; Automatic proving; Mathematics; Logic; Coherence; Truth; Data processing; Paradoxe; Demonstration; Mathematical Logic; Century 20; Assistant de preuve; Programme informatique; Démonstration automatique; Théorie des types; Calculabilité; Mathématiques; Logique; Cohérence; Vérité; Informatique; Paradoxe; Démonstration; Logique mathématique; Siècle 20; Proof assistant; Computer programme; Automatic proving; Mathematics; Logic; Coherence; Truth; Data processing; Paradoxe; Demonstration; Mathematical Logic; Century 20
Publisher: MURS, Paris (FRA)
Date: 2006

This item appears in the following Collection(s)

Show full item record





Advanced Search