Syllabus 2013/2014
 
Extrait PDF Anglais
Français
index
Module : IF105
Titre :
Logique et Preuve
Volumes horaires :
Cours : 9.33 h
Travaux Dirigés : 14.00 h
Travail Individuel : 15.00 h
Crédits ECTS :
2.00
Évaluation :
Enseignant(s) :
HERBRETEAU Frédéric - Responsable
Partagé par l'UE (les UEs) :
Niveau :
module de première année
Résumé :
L'objectif est l'acquisition des outils théoriques permettant de construire un raisonnement formel, ainsi que de prouver la terminaison et la correction des algorithmes.
Plan :
Partie I : Logique
  • Formalisation des énoncés en logique du premier ordre
  • Introduction à la théorie de la preuve
  • Induction, preuve par inducton

    Partie II : Preuve d'algorithmes

  • Spécification: pre/post conditions
  • While-programs, sémantique
  • Preuve de correction partielle : logique de Hoare.
  • Preuve de terminaison : méthode des ensembles bien fondés.
  • Prérequis :
    Aucun
    Document(s) :
    Aucun
    Mot(s) clé(s) :
    Logique, induction, algorithme, correction, terminaison
    Cours en ligne :
    http://www.enseirb-matmeca.fr/~herbrete/IF105