Inf402/Inf432 : introduction à la logique

2024-2025

Équipe enseignante

• Chargé de cours : Benjamin Wack
• groupe INM-01 : Astor Bizard
• groupe INM-02 : Maxime Lesourd
• groupe INM-03 : François Puitg
• groupe MIN-01 : Cristian Ene
• groupe MIN-03 : Nicolas Besson
• groupe MAT-02 : Basile Gros
• groupe MIN-int : Maxime Lesourd

Documents

Supports de cours

Poly de cours et d'exercices
English handout

Projet

Projet par groupes de 3 (éventuellement 4).

• Phase 1 : Modélisation en forme normale conjonctive d'un problème de votre choix
• Phase 2 : Traduction automatique d'une instance de ce problème au format Dimacs à l'aide d'une interface logicielle et utilisation d'un SAT solveur pour résoudre le problème
• Optionnel : Mise au format 3-SAT et écriture d'un SAT solveur non-déterministe

Le sujet détaillé est disponible ci-dessous :

• Sujet du projet
• English project description

Grille indicative de notation du projet
Aide pour le format Dimacs.
Aide pour la réduction SAT vers 3-SAT.
Des idées de problèmes bien adaptés à ce projet :

• Facile :
  • Staircases
  • Easy as ABC
  • N reines
  • Squaro
  • Coloration de graphes
• Moyen :
  • Sudoku
  • Shadows
  • Norinori
  • Futoshiki
  • Takuzu
  • Les problèmes proposés dans ce fichier
  • Certains des problèmes mentionnés sur cette page ou bien sur cette autre page (consulter votre enseignant pour vérifier la faisabilité)
• Difficile :
  • Water Fun
  • Light Up
  • Usowan
  • Kurotto
  • Tetravex
  • Hashiwokakero

Des sujets à éviter, pour des raisons théoriques ou par expérience :

• Trop superficiel : organisation d'un tournoi de football
• Déjà traité de multiples fois les années passées : Tout noir tout blanc, Dosun-Fuwari
• Possible mais très ardu : Camping, Antimorpion, Nonogram
• Problème mal adapté à une modélisation statique : solitaire, dames, échecs, go, taquin, master mind
• Nécessité de calculs difficiles à modéliser : Kakuro

Plan du cours

Documents de cours et séances modifiées

Dans ce planning ne sont reportées que les dates des séances qui diffèrent de l'emploi du temps type.

Enseignement	Transparents en français	Transparents en anglais	Remarques
Cours 1	Transparents du cours	Lesson slides	FR : 13 janvier à 13h30 EN : 13 janvier à 9h45
TDs semaine 1	consulter ADE
Cours 2	Transparents du cours	Lesson slides	FR : jeudi 16 janvier à 13h30 EN : jeudi 16 janvier à 9h45
	Pas de TD le 28 janvier (journée du lycéen)
	QCM d'entraînement chapitre 1 (login avec vos identifiants UGA)
Cours 3	Transparents du cours	Lesson slides
Cours 4	Transparents du cours	Lesson slides
Cours 5	Transparents du cours	Lesson slides
Cours 6	Transparents du cours	Lesson slides
	Quizz d'entraînement chapitres 2 et 3
	Pas de cours ni de TD jeudi 20 février (forum des masters)
Cours 7	Transparents du cours	Lesson slides
Partiels	Partiel d'inf402/inf432 du 10 au 14 mars Pas de cours ni de TD cette semaine
Cours 8	Transparents du cours	Lesson slides
	Quizz chapitre 4
Cours 9	Transparents du cours	Lesson slides
Cours 10	Transparents du cours	Lesson slides
Cours 11	Transparents du cours	Lesson slides
Cours 12	Transparents du cours	Lesson slides
	Quizz chapitre 6
Les derniers cours d'amphi auront lieu le 14/04. Après les derniers cours, le créneau de cours pourra être utilisé pour des rattrapages de TD ou pour les soutenances de projets.

Formule de calcul de la note finale (hors ajustements dûs à la crise sanitaire)

Note finale = 60% CC + 40% Examen

dont CC = 10% Quicks + 20% Partiel + 30% Projet

Ressources

Annales

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

• Sujets de 2023-2024 : Partiel (avec solutions), Session 1 (avec solutions).
• Sujets de 2022-2023 : Partiel (avec solutions), Session 1 (avec solutions).

Outils

• Calculette logique BDDC par Pascal Raymond.
• Une application (Java) pour s'entraîner à construire des démonstrations en déduction naturelle : Peanoware
• Un prouveur en déduction naturelle classique proposé par Michel Levy.
• Un prouveur en résolution binaire au premier ordre proposé par Michel Levy.
• Un site d'entraînement à la formalisation et à la déduction naturelle (inscription obligatoire mais gratuite).

Livres et sites web

• Informatique théorique : logique et démonstration automatique par Michel Lévy, Stéphane Devismes and Pascal Lafourcade

Divers

De 2010 à 2012 ce cours fut enseigné par Pascal Lafourcade.
Jusqu'en 2009 ce cours fut enseigné par Michel Levy.