Sommaire
cours / présentation, démonstration
Du rêve à la réalité des preuves
Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens....
Date de création :
01.08.2011Auteur(s) :
Jean-Paul DelahayeAccéder à la ressource :
Présentation
Informations pratiques
Langue du document : Français
Type : cours / présentation, démonstration
Niveau : enseignement supérieur
Langues : Français
Contenu : texte, image, ressource interactive
Public(s) cible(s) : apprenant
Document : Document HTML
Age attendu : 18+
Droits d'auteur : pas libre de droits, gratuit
Ce document est diffusé sous licence Creative Common : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode
Ce document est diffusé sous licence Creative Common : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode
Description de la ressource
Résumé
Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.
- Granularité : grain
- Structure : atomique
"Domaine(s)" et indice(s) Dewey
- (005.131)
Domaine(s)
- Informatique
- Programmation : Algorithmique, langages, conception objet, programmes
- Informatique
Intervenants, édition et diffusion
Intervenants
Créateur(s) de la métadonnée : Marie-Hélène Comte
Édition
- Institut National de Recherche en Informatique et en Automatique / Interstices
Diffusion
Cette ressource vous est proposée par :
Fiche technique
Identifiant de la fiche : http://ori.unit-c.fr/uid/unit-ori-wf-1-5281
Identifiant OAI-PMH : oai:www.unit.eu:unit-ori-wf-1-5281
Statut de la fiche : final
Schéma de la métadonnée : oai:uved:Cemagref-Marine-Protected-Areas
- LOMv1.0
- LOMFRv1.0
- SupLOMFRv1.0
- Voir la fiche XML
Entrepôt d'origine : UNIT
Voir aussi
11.12.2008
Description
:
Peut-on être sûr de la vérité d’une preuve ? Cette preuve de la preuve, comment l’obtenir en pratique ? La vérification formelle de démonstration est de plus en plus utilisée par les mathématiciens.
- preuve de programme
- preuve formelle
- logique mathématique
- démonstration
- Coq
- théorème des quatre couleurs
- fuscia
21.09.2012
Description
:
Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
- Coq
- assistant de preuve
- programmation fonctionnelle sûre
- preuve de programme
- logique mathématique
- méthode formelle
- calcul des constructions
- correction de logiciel
- algorithmique certifiée
- théorie des types
- logiciel libre
- récursion
- fuscia