Pascal Lafourcade

MODULE INF242 : Introduction à la logique (base de la démonstration automatique)

2010 - 2011

Lien ADE
Programme du module :

• Introduction
• Logique Propositionnelle:
  • Table de vérité, forme normale
  • Résolution
  • Déduction naturelle
• Logique du premier ordre:
  • Résolution
  • Complétude
  • Déduction naturelle

Poly .pdf

Équipe enseignante:

• Pascal Lafourcade COURS : Vendredi 8h00 - 9h45, Amphi E1
• Martin Gagné ENGLISH COURSE / Thursday 15h15 - 16h45, E202
• Mathilde Duclos ENGLISH TD / Monday 15h15 - 16h30 A102 and Thursday 8h00 - 9h45 D104
• Puitg Francois Grpe INF-S4-01 Grpe INF-S4-02. Mercredi 9h45 - 11h15 A101 et Jeudi 15h15 - 16h45 E207.
• Selma Saidi Grpe MAT-S4 Grpe MIN-S4-02. Lundi 8h00-9h30 D104 et Mercredi 15h15-16h45 B006.

Cours

Pour imprimer en 2, 4, 6, 9 et 16 par pages avec Acroread il faut choisir dans page scaling : Multipage per sheet et le nombre de pages voulues.

TD	Date	Heure	Salle	Slides	Commentaires
1	Mercredi 27 Janvier 2010	8h00 - 9h30	DLST - A2	cours 1	Distribution Poly + Projet
2	Jeudi 28 Janvier 2010	15h15 - 16h45	DLST - E2	cours 2
3	Mercredi 3 Février 2010	8h00 - 9h30	DLST - A2	cours 3
4	Jeudi 4 Février 2010	15h15 - 16h45	DLST - E2	cours 4
5	Jeudi 11 Février 2010	15h15 - 16h45	DLST - E2	cours 5
6	Jeudi 25 Février 2010	15h15 - 16h45	DLST - E2	cours 6	Goedel How to make a presentation
7	Jeudi 4 Mars 2010	15h15 - 16h45	DLST - E2	cours 7
8	Jeudi 11 Mars 2010	15h15 - 16h45	DLST - E2	cours 8
9	Jeudi 18 Mars 2010	15h15 - 16h45	DLST - E2	cours 9 cours 9bis	dernier cours avant le partiel
10	Jeudi 8 Avril 2010	15h15 - 16h45	DLST - E2	cours 10
11	Jeudi 22 Avril 2010	15h15 - 16h45	DLST - E2	cours 11
12	Jeudi 29 Avril 2010	15h15 - 16h45	DLST - E2	cours 12	Dernier cours

Formule de calcul de la note finale

Note finale=40%CC+60%Examen

CC = 10% Quicks + 40% Partiel + 50% Projet.

Projet

Grille de notation du projet Projet par groupe de 3 ou 4.

• Phase 1 : Modélisation en formule Dimacs d'un problème de votre choix
• Phase 2 : Utilisation d'un SAT solveur pour résoudre le problème.

Aide pour le format Dimacs.
Planning cf Sujet du Projet .pdf

Annales

Les solutions sont minimalistes et ne constituent pas un modèle de rédaction.

• Sujets de 2008-2009 : Session 1
• Sujets de 2009-2010 : Partiel, Solutions, Session 1 Solutions et Session 2 Solutions

Divers

Ce cours fut enseigné par Michel Levy jusqu'en 2009.

Année 2009-2010

Année 2010-2011

Ici un prouveur classique proposé par Michel Levy.

Calculette logique BDDC dé par Pascal Raymond.

---