Course Syllabus 2013/2014
 
PDF Extract Anglais
Français
index
Module : IF105
Title :
Logic and proof
Number of hours :
Lecture : 9.33 h
Tutorial classes : 14.00 h
Individual work : 15.00 h
ECTS credits :
2.00
Evaluation :
S1: ET(2h,E,fa,sc) x1; S2: ET(2h,E,fa,sc) x1   Detail of the nomenclature used for the creation of the evaluation code
Teacher(s) :
HERBRETEAU Frédéric - Responsible
Shared by UV(s) :
Level :
first year module
Abstract :
The goal is to acquire theoretical tools in order to build formal reasonings, and to prove the termination and the correction of algorithms.
Plan :
1st part : Logic
  • formalization in first-order logic
  • introduction to proof theory
  • induction, proof by induction

    2nd part : proofs of algorithms

  • specification through pre and post conditions
  • while-programs, semantics
  • proof of correctness, Hoare's logic
  • termination proof: well-founded sets
  • Prerequisite :
    None
    Document(s) :
    None
    Keyword(s) :
    Logic, induction, algorithms, correctness, termination
    Online course :
    http://www.enseirb-matmeca.fr/~herbrete/IF105