Introduction à la logique et démonstration automatique - Université Grenoble Alpes (UGA, L2, INF402)

Résumé de section

• Sélectionner la section Informations générales

  Replier Déplier

  Informations générales

  Tout replier Tout déplier

  If you speak English but see this site in French, please change your language settings in your user preferences.

  • Sélectionner l’activité Announcements

    

    Announcements Forum
  • Sélectionner l’activité Équipe enseignante Chargé de cours : Benjamin Wack...

    Équipe enseignante

    • Chargé de cours : Benjamin Wack
    • groupe INM-01 : Astor Bizard
    • groupe INM-02 : Cristian Ene
    • groupe INM-03 : Matthieu Petiteau
    • groupe MIN-01 : Cristian Ene
    • groupe MIN-03 : Benjamin Gaudin
    • groupe MAT-02 : François Puitg
    • groupe MIN-int : Aleksei Gorelov

    Supports de cours

    • Poly de cours et d'exercices
    • English handout

    Évaluation

    • 10% Quicks (brèves interros durant les TDs)
    • 20% Partiel
    • 30% Projet
    • 40% Examen
      

    Projet

    Par groupes de 3 (éventuellement 4)

    • Phase 1 : Modélisation en forme normale conjonctive d'un problème de votre choix
    • Phase 2 : Programmation d'une interface logicielle pour traduire automatiquement tout instance de ce problème au format Dimacs 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)

    Sujet détaillé

    • Sujet du projet
    • English project description

    Autres documents liés au projet

    • Grille indicative de notation
    • 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 :
      • Easy as ABC
      • N reines
      • Mosaic
      • Squaro
      • Coloration de graphes
    • Moyen :
      • Fill-a-Pix
      • Sudoku
      • Norinori
      • Futoshiki
      • Makaro
      • Takuzu
      • Les problèmes proposés dans ce fichier
      • Certains des problèmes mentionnés sur cette page (consulter votre enseignant pour vérifier la faisabilité)
    • Difficile :
      • Juosan
      • Tents
      • Light Up
      • Usowan
      • Hitori
      • Kurotto
      • Tetravex
    • 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, Hashiwokakero
      • 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

  • Sélectionner l’activité Soutenances projet

    

    Soutenances projet Livre
  • Sélectionner l’activité Inscription groupe TD

    

    Inscription groupe TD Choix de Groupe

    Disponible à partir du 12 janvier 2026
• Sélectionner la section Logique propositionnelle

  Replier Déplier

  Logique propositionnelle
• Sélectionner la section Résolution propositionnelle

  Replier Déplier

  Résolution propositionnelle
• Sélectionner la section Déduction naturelle

  Replier Déplier

  Déduction naturelle
• Sélectionner la section Logique du premier ordre

  Replier Déplier

  Logique du premier ordre
• Sélectionner la section Méthode de Herbrand, résolution au premier ordre

  Replier Déplier

  Méthode de Herbrand, résolution au premier ordre
• Sélectionner la section Déduction naturelle au premier ordre

  Replier Déplier

  Déduction naturelle au premier ordre
• Sélectionner la section Ressources

  Replier Déplier

  Ressources

  • Sélectionner l’activité Annales Les solutions sont minimalistes et ne cons...

    Annales

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

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

    Outils

    • Calculette logique BDDC par Pascal Raymond.
    • 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.