34 résultats : preuves

Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern)

Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern)

Description : Les outils de vérification formelle de programmes (analyseurs statiques, prouveurs de programmes, model-checkers) ont fait des progrès remarquables ces dernières années et commencent à percer dans le monde du logiciel critique. Cependant, ces outils ne vérifient "que" des programmes source: des ...

Mots clés : compilateur, logiciel critique, programmation fonctionnelle, vérification de programme, vérification formelle, preuve formelle, fuscia, conference, stic, recherche

Date : 08-10-2009

Droits : Document libre, dans le cadre de la licence Creative Commons (http://creativecommons.org/licenses/by-nd/2.0/fr/), citation de l'auteur obligatoire et interdiction de désassembler (paternité, pas de modification)

Comment faire confiance à un compilateur ?

Comment faire confiance à un compilateur ?

Description : Comment faire exécuter par une machine des programmes écrits dans un langage de haut niveau, qu’elle ne peut comprendre ?

Mots clés : erreur, langage haut niveau, fossé sémantique, preuve formelle, CompCert, fuscia

Date : 30-03-2010

Droits : 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

Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange

Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange

Description : Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange. In "La vérité", Journées Scientifiques annuelles de l'Institut Universitaire de France, organisées par le Pôle de recherche et d'enseignement supérieur (PRES) de Toulouse, l'U ...

Mots clés : catastrophe naturelle, géomorphologie, paléoenvironnement, connaissance scientifique, causalité, Environnement et risques, archéologie littorale, preuve (épistémologie)

Date : 03-04-2013

Les leçons d’un algorithme délinquant

Les leçons d’un algorithme délinquant

Description : Pour le sens commun, la machine ne se trompe jamais. Si par malheur un utilisateur pointilleux découvre une erreur dans son calcul sur ordinateur, qui doit-il alors accuser ? Lui, ou la machine ?

Mots clés : bug, Pentium, implémentation d'algorithmes, erreur, preuve formelle, fuscia

Date : 19-02-2004

Droits : 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

RMJCA N6 - De la scène de crime à la preuve génétique - IFEG

RMJCA N6 - De la scène de crime à la preuve génétique - IFEG

Description : Le docteur Olivier PASCAL, Président de l'Institut Français des Empreintes Génétiques (IFEG) et Monsieur Eric TABARY Directeur de l'IFEG, montrent quelle est l'utilité des empreintes génétiques en tant que preuve.

Mots clés : ADN, preuves, Faculté de Médecine de Reims, Manifestation de la Vérité

Date : 15-05-2009

Droits : Droits réservés à l'éditeur et aux auteurs.

Proofs assistants : from symbolic logic to real mathematics

Proofs assistants : from symbolic logic to real mathematics

Description : Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally developed ...

Mots clés : preuve de programme

Date : 18-05-2017

Droits : Droits réservés à l'éditeur et aux auteurs.

Introduction à la logique

Introduction à la logique

Description : Ce cours a pour but d'introduire la notion de logique en programmation. Voici les notions abordées : * définition de la logique, * calcul des propositions (si ... et ... alors...), * les preuves, * le calcul des prédicats, * la logique intuitionniste * le lambda-calcul.

Mots clés : logique, langage formel, algèbre Boole, calcul proposition, algorithme de décision, preuve, calcul prédicat, logique intuitionniste, lambda calcul, fuscia

Date : 01-09-2009

Droits : Ressource en accès libre.

Gaz de schistes : quelles vérités ? / François Renard, Bénédicte Fauvarques-Cosson

Gaz de schistes : quelles vérités ? / François Renard, Bénédicte Fauvarques-Cosson

Description : Gaz de schistes : quelles vérités ? / François Renard, Bénédicte Fauvarques-Cosson. In "La vérité", Journées Scientifiques annuelles de l'Institut Universitaire de France, organisées par le Pôle de recherche et d'enseignement supérieur (PRES) de Toulouse, l'Université Toulouse II-Le Mirail et l' ...

Mots clés : connaissance scientifique, objectivité, vérité (épistémologie), gaz de schiste, expert scientifique, conseillers scientifiques, sécurité juridique, preuve (épistémologie)

Date : 02-04-2013

L'Ecole d'Été Méditerranéenne d'Information en Santé (EEMIS) : Bonnes pratiques(7)

L'Ecole d'Été Méditerranéenne d'Information en Santé (EEMIS) : Bonnes pratiques(7)

Description : Intervention de Brigitte Seroussi. On observe une grande diversité des pratiques médicales. Il faut intégrer une expertise individuelle à l'evidence-based-medicine. Les guidelines sont des recommandations pour aider le médecin dans sa pratique, ce sont des documents textuels et numériques. Sont ...

Mots clés : modélisation, bonnes pratiques, qualité des données, pratique médicale, norme, SI, ingénierie de la santé, aide à la décision, droits du patient, évaluation, système d'information, rationalité, santé, éthique, niveau de preuve

Date : 20-07-2005

Droits : Droits réservés à l'éditeur et aux auteurs.

Approches fonctionnelles de la programmation

Approches fonctionnelles de la programmation

Description : Fournir un panorama complet du paradigme de programmation fonctionnelle et de son positionnement par rapport aux autres paradigmes de programmation (en particulier de la programmation impérative). Illustrer l'ensemble des concepts abordés au moyen de deux langages fonctionnels: Lisp et Haskell.

Mots clés : fuscia, Lisp, Haskell, preuve de programme

Date : 07-01-2009

La vérité et la machine

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.

Mots clés : preuve de programme, preuve formelle, logique mathématique, démonstration, Coq, théorème des quatre couleurs, fuscia

Date : 11-12-2008

Droits : 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

La vérité et la machine

Évaluation polynomiale [pf03] - Exercice

Évaluation polynomiale [pf03] - Exercice

Description : Cet exercice détermine la complexité de l'évaluation polynomiale selon le schéma de Hörner.

Mots clés : Preuve d'algorithme, Notations asymptotiques, algorithmie, programmation, C, C++, Java

Date : 10-2010

Droits : Licence creative commons de type 3:http://creativecommons.org/licenses/by-nc-sa/3.0/deed.fr - pour plus d'information contacter l'auteur

L'ordinateur au cœur de la découverte mathématique

L'ordinateur au cœur de la découverte mathématique

Description : L’ordinateur joue un rôle essentiel dans le travail du mathématicien, en lui permettant de gérer la complexité de certaines preuves.

Mots clés : mathématiques pour l'informatique, calcul formel, théorème des quatre couleurs, mathématiques discrètes, coloration graphe, preuve par ordinateur, fuscia

Date : 01-09-2011

Droits : 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