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

Perfilado de sección

• Seleccionar sección General information

  Colapsar Expandir

  General information

  Colapsar todo Expandir todo

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

  • Seleccionar actividad Announcements

    

    Announcements Foro
  • Seleccionar actividad Équipe enseignante Chargé de cours : Benjamin Wack...

    Teaching team

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

    Teaching material

    • English handout

    Evaluation

    • 10% Quicks tests (during TDs)
    • 20% Midterm
    • 30% Project
    • 40% Exam

    Project

    Groups of 3 (4 at worst)

    • Phase 1 : Modelization the problem your choose in conjunctive normal form
    • Phase 2 : Programming a software interface for converting automatically any instance of that problem into Dimacs format and using a SAT solver to solve the problem
    • Optional : Transformation into 3-SAT format and programming of a (non-deterministic) SAT solver

    Detailed subject

    • English project description

    Other documents for the project

    • Grading indications
    • Help for the Dimacs format
    • Help for reduction SAT to 3-SAT.

    Problem ideas suitable for this project

    • Easy:
      • Easy as ABC
      • Mosaic
      • No four in a row
      • Gappy
      • Eulero
      • Numbrix
    • Intermediate:
      • Magnets
      • Bricks
      • Norinori
      • Makaro
      • Some of the problems listed in this file or on that page (check feasability with your teacher)
    • Hard:
      • Juosan
      • Tents
      • Light Up
      • Usowan
      • Hitori
      • Kurotto
      • Tetravex
    • Problems to be avoided:
      • Studied too often: Tout noir tout blanc, Dosun-Fuwari, Hashiwokakero, N reines, Squaro, graph colouring, Sudoku, Takuzu, Futoshiki
      • Possible but really tricky: Camping, Antimorpion, Nonogram
      • Unsuitable for a static modelization: solitaire, draughts, chess, go, 15 puzzle, master mind
      • Requires arithmetic computations: Kakuro
  • Seleccionar actividad Project defenses

    

    Project defenses Libro
  • Seleccionar actividad TD group subscription

    

    TD group subscription Elección de grupo
• Seleccionar sección Propositional logic

  Colapsar Expandir

  Propositional logic

  • Seleccionar actividad Transparents de cours semaine 1 Lesson slides week...

    • Lesson slides week 1
  • Seleccionar actividad Transparents de cours semaine 2 Lesson slides week...

    • Lesson slides week 2
  • Seleccionar actividad Test de logique propositionnelle

    

    Test de logique propositionnelle Cuestionario
• Seleccionar sección Propositional resolution

  Colapsar Expandir

  Propositional resolution

  • Seleccionar actividad Transparents de cours semaine 3 Lesson slides week...

    • Lesson slides week 3
  • Seleccionar actividad Transparents de cours semaine 4 Lesson slides week...

    • Lesson slides week 4
  • Seleccionar actividad Test de résolution

    

    Test de résolution Cuestionario
• Seleccionar sección Natural deduction

  Colapsar Expandir

  Natural deduction

  • Seleccionar actividad Transparents de cours semaine 5 Lesson slides week...

    • Lesson slides week 5
  • Seleccionar actividad Transparents de cours semaine 6 Lesson slides week...

    • Lesson slides week 6
  • Seleccionar actividad Test de déduction naturelle

    

    Test de déduction naturelle Cuestionario
• Seleccionar sección First-order logic

  Colapsar Expandir

  First-order logic

  • Seleccionar actividad Transparents de cours semaine 7 Lesson slides week...

    • Lesson slides week 7
• Seleccionar sección Herbrand's method, first-order resolution

  Colapsar Expandir

  Herbrand's method, first-order resolution
• Seleccionar sección First-order natural deduction

  Colapsar Expandir

  First-order natural deduction
• Seleccionar sección Resources

  Colapsar Expandir

  Resources

  • Seleccionar actividad Annales Les solutions sont minimalistes et ne cons...

    Archives

    The provided solutions are minimalistic and do not reflect the expected level of writing.

    • 2024-2025 Subjects: Midterm (with solutions), 1st Session (with solutions).
    • 2023-2024 Subjects: Midterm (with solutions), 1st Session (with solutions).

    Tools

    • Logic calculator BDDC by Pascal Raymond.
    • A classical natural deduction prover offered by Laurent Théry.
      Also available as an Android app.
    • A classical natural deduction prover offered by Michel Levy.
    • A first-order binary resolution prover offered by Michel Levy.
    • A training website for formalization and natural deduction (subscription is mandatory but free).

    Books and web sites

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

    Miscellaneous

    From 2010 to 2012 this lecture was given by Pascal Lafourcade.
    Until 2009 it was taught by Michel Levy.