Logique du premier ordre

Révisions

Florent Capelli

Examen

Rappel : examen le 27 mars de 10h à 12h.

  • De la logique propositionnelle
  • Et de la logique du premier ordre

Logique propositionnelle

Connaissance générales

  • Formule propositionnelle
  • Tables de vérité
  • Lois de De Morgan, distributivité etc.
  • Formes normales : conjonctive (FNC), disjonctive (FND).
    • connaître les définitions
    • savoir mettre une formule sous forme normale
  • Sémantique d’une formule étant donnée une interprétation
    • Modèles et contre-modèle d’une formule
    • Validité d’une formule / formule contradictoire
  • Ensembles de connecteurs fonctionnellement complets :
    • {∧,¬}.
    • {∨,¬}.
    • {NAND}.
  • Lien sémantique et satisfiabilité.

Modélisation et SAT Solving

  • Être capable de modéliser un problème en logique propositionnel
  • Connaître le fonctionnement général des SAT solvers: DPLL, CDCL
  • Principe de résolution pour les FNC
    • schéma de fusion : ℓ ∨ ℓ ∨ C ≡ ℓ ∨ C
    • schéma de résolution
    • complétude de la résolution (pour contradiction)

Compétences

  • Savoir manipuler syntaxiquement les formules
    • lois de de Morgan
    • mise sous FNC, FND
  • Savoir modéliser en logique propositionnelle
    • traduire un énoncé en français vers une formule de la logique propositionnelle équivalent
    • savoir trouver les modèles d’une petite formule propositionnelle (table de vérité)
  • Savoir trouver une preuve de contradiction d’une (petite) formule en utilisant la résolution.

Logique du premier ordre

Syntaxe

  • Langage du premier ordre :
    • symboles de prédicats
    • constantes
    • symboles de fonctoins
  • Connaître la syntaxe de la LPO :
    • notion de terme
    • notion de formule

Manipulation des formules

  • Savoir écrire l’arbre syntaxique d’une formule
  • Savoir repérer les variables libres d’une formule
  • Savoir renommer les variables liées sans capture
  • Savoir substituer des variables libres par des termes, sans capture.
  • Savoir manipuler syntaxiquement les formules :
    • Dualité des quantificateurs ∀ϕ et ¬∃¬ϕ
    • Lois de De Morgan etc.
    • Mise sous forme prénexe.

Sémantique

  • Savoir ce que c’est qu’une interprétation d’un langage du premier ordre.
  • Notion de théorème (validité), modèle et de contre-modèle d’une formule ϕ :
    • Savoir calculer la valeur d’une formule dans un modèle M simple.
    • Connaître les notations : M ⊨ ϕ,  ⊨ ϕ.
    • Savoir construire un modèle et un contre-modèle d’une formule simple.
  • Savoir traduire des énoncés en français vers la logique du premier ordre et vice versa.
  • Savoir ce qu’est une skolemization.

Théorie des modèles

  • Connaître la notion de théorie
  • Notion de modèles et théorème dans une théorie
  • Calcul des séquents :
    • Comprendre les liens une preuve dans LK et la validité d’une formule
    • Comprendre ce que veut dire le théorème de complétude.
    • Savoir faire une petite preuve dans LK.

Prolog

  • Unification
    • Comprendre la définition d’un problème d’unification.
    • Savoir calculer un unificateur le plus général de deux termes.
  • Prolog
    • Connaître le terme contraintes de Horn.
    • Comprendre la sémantique d’un programme prolog simple.
    • Comprendre les liens entre l’unification et l’inférence de prolog.