Introduction to logic and automated proof (UGA, L2, INF432)

Section outline

• Выбрать секцию General information

  Свернуть Развернуть

  General information

  Свернуть всё Развернуть всё

  Si vous parlez français mais que vous voyez ce site en anglais, pensez à paramétrer la langue dans votre profil utilisateur.

  • Выбрать элемент Announcements

    

    Announcements Форум
  • Выбрать элемент É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

  • Выбрать элемент Soutenances projet

    

    Soutenances projet Книга
  • Выбрать элемент Inscription groupe TD

    

    Inscription groupe TD Выбор группы

    Доступно с 12 января 2026
• Выбрать секцию

  Свернуть Развернуть
• Выбрать секцию Propositional resolution

  Свернуть Развернуть

  Propositional resolution
• Выбрать секцию Natural deduction

  Свернуть Развернуть

  Natural deduction
• Выбрать секцию First-order logic

  Свернуть Развернуть

  First-order logic
• Выбрать секцию Herbrand's method, first-order resolution

  Свернуть Развернуть

  Herbrand's method, first-order resolution
• Выбрать секцию First-order natural deduction

  Свернуть Развернуть

  First-order natural deduction
• Выбрать секцию Resources

  Свернуть Развернуть

  Resources

  • Выбрать элемент 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.