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 première partie .pdf
Poly seconde partie .pdf

Équipe enseignante:

• Pascal Lafourcade COURS
• Philippe Bidinger
• Mathilde Duclos
• Puitg Francois

Cours

Les cours ont lieus habituellement jeudi de 15h15 à 16h45 amphi E2 au DLST.

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 3-sat SAT-3SAT
• Phase 2 : Réalisation d'un DP ou SC et d'un Walk-Sat ou G-sat Wikipedia

Aide pour le format Dimacs.
Planning

• A la fin de la deuxième semaine de TD consitution des groupes et choix des sujets.
• Livraison par email à votre enseignant de TD au plus tard le 1er avril 2010 à minuit du pré-rapport.
• Livraison le lundi 9 mai 2010 à minuit par email du rapport final.
• Soutenance du Projet : le mardi 10 mai 2010 de 8h00 à 12h00 salle b105 b106 b106bis

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

Ici un prouveur classique proposé par Michel Levy.

Calculette logique BDDC dé par Pascal Raymond.

---