UE Introduction à la logique (INF 452)

•  Logique propositionnelle :
   • Syntaxe et sémantique
   • Algèbre de Boole : structure mathématique sous-jacente
   • Transformations de formules
   • Étude de la validité d'une proposition par une méthode algorithmique
• Vers la logique du premier ordre (LPO)
   • Étude de la validité d'un énoncé par une méthode déductive
• Sémantique de la logique du premier ordre (LPO)
   • Domaine, interprétation
   • Construction de modèle
   • Lois de manipulation des quantificateurs
   • Résolution au premier ordre

Objectifs : 

• Maîtriser la syntaxe et la sémantique de la logique propositionnelle et de la logique du premier ordre.
• Savoir formaliser des raisonnements en logique.
• Être capable d’utiliser des méthodes formelles comme la résolution, les preuves par déduction naturelle, et les preuves en arbre.
• Appliquer ces connaissances à des systèmes de démonstration automatique ou des solveurs (SAT, DPLL, etc.).

• Notions de base en mathématiques discrètes (ensembles, fonctions, relations)
• Compréhension du raisonnement mathématique (implication, équivalence, raisonnement par l’absurde)
• Bases en algorithmique et programmation (pour l’utilisation ou la conception d’outils automatiques)

• Logique propositionnelle
  - Syntaxe et sémantique
  - Tableaux de vérité
  - Équivalences logiques
  - Formes normales (FNC, FND)
  - Résolution propositionnelle
  - DPLL (Davis–Putnam–Logemann–Loveland)

• Démonstration automatique
  - Déduction naturelle
  - Preuves en arbre (type Gentzen)
  - SAT solveurs : encodage, résolveurs

• Logique du premier ordre
  - Syntaxe (quantificateurs, variables)
  - Sémantique (structures, interprétations)
  - Skolémisation 
  - Théorème de Herbrand
  - Résolution en logique du premier ordre

• Applications
  - Modélisation de problèmes (Sudoku, logique de jeu, etc.)
  - Résolution automatique via un solveur SAT ou Prolog

Formes d'enseignement : 

• CM
• TD
• Projet
• Evaluation (projet groupe, soutenance projet, QCM, partiel, examen final, etc)

Connaissances visées : 

• Validité d'un raisonnement 
• Notions de correction et de complétude 
• Bases théoriques de la programmation logique 
•  Liens entre : circuits et formules propositionnelles ; conséquence et preuve.

Compétences visées :

• Utilisation de systèmes formels 

•  Formalisation en logique
•  Techniques de démonstration
•  Manipulations symboliques : règles formelles, unification,..

Architectures logicielles et matérielle,  Amblard, Fernandez, Lagnier, Maraninchi, Sicard, Waille, Dunod, 2000.