Archives du mot-clé : preuve_formelle

C@fé-in (23 février) : Pourquoi faire appel à un ordinateur pour faire des preuves?

 

23 Février 2012, 13h15 – 14h, salle cafétéria extension, par Yves Bertot

Nous faisons tous des raisonnements pour prendre des décisions dans notre vie de tous les jours mais ces raisonnements ne sont pas toujours justes.  La logique, c’est l’art de reconnaître les raisonnements justes, indépendamment du sujet traité.    On utilise des règles systématiques qui peuvent être reconnues par ordinateur.

Pour savoir si un programme est correct, on peut le faire par des raisonnements, mais ceux-ci sont longs et fastidieux.  C’est un travail pénible et répétitif, c’est mieux si ça peut être fait par ordinateur.

Transparents de la présentation

Lien Permanent pour cet article : https://project.inria.fr/mastic/pourquoi-faire-appel-a-un-ordinateur-pour-faire-des-preuves/