INFO-F-302: Informatique Fondamentale


Ce cours porte sur la logique en informatique (logique propositionnelle et logique du premier ordre), et une introduction à la calculabilité sera donnée. Il est basé sur le cours INFO-F-302 Logique Informatique des années précédentes.

Chargé de cours pour l'année 2011-2012: Emmanuel Filiot, bureau NO8.110, en remplacement du Pr. Jean-François Raskin.
Chargé de TP pour l'année 2011-2012: Alexander Heussner., bureau NO8.207.

Calendrier Prévisionnel - horaire 2012

Mardis, 14:00 - 16:00
Jeudis, 8:00 - 10:00.

Mardi 7 février Cours P.A2.120 Jeudi 9 février Cours P.FORUM.F
Mardi 14 février Cours P.A2.120 Jeudi 16 février TP P.FORUM.F
Mardi 21 février mardi gras Jeudi 23 février Cours P.FORUM.F
Mardi 28 février TP P.A2.120 Jeudi 1 mars Cours P.FORUM.F
Mardi 6 mars TP P.A2.120 Jeudi 8 mars Cours P.FORUM.F
Mardi 13 mars Cours P.A2.120 Jeudi 15 mars TP P.FORUM.F
Mardi 20 mars Cours (Tampon, salle à réserver) Jeudi 22 mars TP (Tampon) FORUM G
Mardi 27 mars Cours P.A2.120 Jeudi 29 mars Cours ou TP (par Mr Filiot) P.OF.2070
Mardi 3 avril Vacances Jeudi 5 avril Vacances
Mardi 10 avril Vacances Jeudi 13 avril Vacances
Mardi 17 avril Cours P.A2.120 Jeudi 19 avril TP P.OF.2070
Mardi 24 avril Cours P.A2.120 Jeudi 26 avril TP P.OF.2070
Mardi 1 mai Férié Jeudi 3 mai Cours ou TP P.OF.2070
Mardi 8 mai Cours P.A2.120 Jeudi 10 mai Cours ou TP P.OF.2070
Mardi 15 mai Tampon P.A2.120 Jeudi 17 mai Ascension
Mardi 22 mai Tampon P.A2.120 Jeudi 24 mai Tampon

Support de cours

Transparents

Support de cours des années précédentes

Slides du cours
Formulaire disponible à l'examen

Travaux pratiques

Séance 1 : Les tableaux sémantiques − Solutions
Séance 2 : La déduction naturelle − Solutions
Séance 3 : La résolution − Solutions
Séance 4 : La logique du premier ordre − Solutions
Séance 5 : La résolution dans la logique du premier ordre − Solutions
Séance 6 : Les modèles de Herbrand − Solutions
Séance 7 : Programmation logique − Solutions
Séance 8 : La déduction naturelle dans la logique du premier ordre − Solutions

Projet d'année (2011): Jeu ABCPath et Solveurs SAT

Code pour la résolution du Sudoku avec Minisat, sujet PDF, Exemples de grilles.

Projet d'année (2010): Enigme d'Einstein et le Solveur de Logique du Premier Ordre Paradox

sujet PDF, exemple de fichier TPTP (pour la résolution des grilles de Sudoku), Spécification Paradox pour l'énigme.

Projet d'année (2009)

Enoncé du projet − Exemple de solution − Exemple de code
Archive contenant tous les fichiers du projet: