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é Inscription groupe de travail projet

    

    Inscription groupe de travail projet Choix de Groupe

    Merci de vous inscrire dans un des groupes de travail ci-dessous. Effectifs mini/maxi = 3/4.

    En cas de non-inscription (ou de monôme ou de binôme), sauf cas particulier vu avec votre enseignant de TD, vous pourrez être affecté d'office à un groupe.

  • 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
    • group MIN-int: Aleksei Gorelov

    Supports de cours

    • Poly de cours et d'exercices

    É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

    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
      • Mosaic
      • No four in a row
      • Gappy
      • Eulero
      • Numbrix
    • Moyen :
      • Magnets
      • Bricks
      • Norinori
      • Makaro
      • Certains des problèmes mentionnés dans ce fichier ou 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 :
      • Traité trop de fois : Tout noir tout blanc, Dosun-Fuwari, Hashiwokakero, N reines, Squaro, coloration de graphes, Sudoku, Takuzu, Futoshiki
      • 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 arithmétiques, pénibles à 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
• Sélectionner la section Logique propositionnelle

  Replier Déplier

  Logique propositionnelle

  • Sélectionner l’activité Transparents de cours semaine 1 Lesson slides week...

    • Transparents de cours semaine 1
  • Sélectionner l’activité Transparents de cours semaine 2 Lesson slides week...

    • Transparents de cours semaine 2
  • Sélectionner l’activité Test de logique propositionnelle

    

    Test de logique propositionnelle
• Sélectionner la section Résolution propositionnelle

  Replier Déplier

  Résolution propositionnelle

  • Sélectionner l’activité Transparents de cours semaine 3 Lesson slides week...

    • Transparents de cours semaine 3
  • Sélectionner l’activité Transparents de cours semaine 4 Lesson slides week...

    • Transparents de cours semaine 4
  • Sélectionner l’activité Test de résolution

    

    Test de résolution
• Sélectionner la section Déduction naturelle

  Replier Déplier

  Déduction naturelle

  • Sélectionner l’activité Transparents de cours semaine 5 Lesson slides week...

    • Transparents de cours semaine 5
  • Sélectionner l’activité Transparents de cours semaine 6 Lesson slides week...

    • Transparents de cours semaine 6
  • Sélectionner l’activité Test de déduction naturelle

    

    Test de déduction naturelle
• Sélectionner la section Logique du premier ordre

  Replier Déplier

  Logique du premier ordre

  • Sélectionner l’activité Transparents de cours semaine 7 Lesson slides week...

    • Transparents de cours semaine 7
  • Sélectionner l’activité Transparents de cours semaine 8 Lesson slides week...

    • Transparents de cours semaine 8
  • Sélectionner l’activité Quiz d'entraînement en logique du premier ordre

    

    Quiz d'entraînement en logique du premier ordre Test
• 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 l’activité Transparents de cours semaine 9 Lesson slides week...

    • Transparents de cours semaine 9
• 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.
    • Une appli web pour construire des arbres de preuve en déduction naturelle classique proposée par Laurent Théry.
      Également disponible sous forme d'application Android.
    • 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.