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

Представяне по теми

• Informations générales

  Сгъване на всички Разгъване на всички
  • 

    Announcements Форум
  • É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

    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 :
      • 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

  • 

    Inscription groupe TD Група за избор

• Logique propositionnelle
  • • Transparents de cours semaine 1
    • Lesson slides week 1
      
  • • Transparents de cours semaine 2
    • Lesson slides week 2
      
  • 

    Test de logique propositionnelle Тест

• Résolution propositionnelle
  • • Transparents de cours semaine 3
    • Lesson slides week 3
      
  • • Transparents de cours semaine 4
    • Lesson slides week 4
      

• Déduction naturelle

• Logique du premier ordre

• Méthode de Herbrand, résolution au premier ordre

• Déduction naturelle au premier ordre

• 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.
    • 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.