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

Section outline

• Select section General information

  Collapse Expand

  General information

  Collapse all Expand all

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

  • Select activity Inscription groupe de travail projet

    

    Inscription groupe de travail projet Group choice

    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.

  • Select activity Announcements

    

    Announcements Forum
  • Select activity É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
  • Select activity Project defenses

    

    Project defenses Book
  • Select activity TD group subscription

    

    TD group subscription Group choice

    Available until 7 March 2026, 11:55 PM
• Select section Propositional logic

  Collapse Expand

  Propositional logic

  • Select activity Transparents de cours semaine 1 Lesson slides week...

    • Lesson slides week 1
  • Select activity Transparents de cours semaine 2 Lesson slides week...

    • Lesson slides week 2
  • Select activity Test de logique propositionnelle

    

    Test de logique propositionnelle Quiz
• Select section Propositional resolution

  Collapse Expand

  Propositional resolution

  • Select activity Transparents de cours semaine 3 Lesson slides week...

    • Lesson slides week 3
  • Select activity Transparents de cours semaine 4 Lesson slides week...

    • Lesson slides week 4
  • Select activity Test de résolution

    

    Test de résolution Quiz
• Select section Natural deduction

  Collapse Expand

  Natural deduction

  • Select activity Transparents de cours semaine 5 Lesson slides week...

    • Lesson slides week 5
  • Select activity Transparents de cours semaine 6 Lesson slides week...

    • Lesson slides week 6
  • Select activity Test de déduction naturelle

    

    Test de déduction naturelle Quiz
• Select section First-order logic

  Collapse Expand

  First-order logic

  • Select activity Transparents de cours semaine 7 Lesson slides week...

    • Lesson slides week 7
• Select section Herbrand's method, first-order resolution

  Collapse Expand

  Herbrand's method, first-order resolution
• Select section First-order natural deduction

  Collapse Expand

  First-order natural deduction
• Select section Resources

  Collapse Expand

  Resources

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