Logique et Calculabilité (2017)


Intervenants

Luigi Santocanale et Kevin Perrot.

Infos

Emploi du temps

Le calendrier sciences de AMU.
Organisation du cours : 2h *10 cours, 3h*10 TDs, 2h*5 TPs.
  1. 16/01/2017 : Calcul propositionnel, syntaxe et sémantique. Valuation, modèle, formule (in)satisfaisable, contradictoire, tautologie, relations d'équivalence logique et de conséquence logique entre formules.
  2. 23/01/2017 : Conséquence logique d'un ensemble de formules. Propriétés de la conséquence logique. Théorème de compacité. Équivalences élémentaires entre formules propositionnelles.
  3. 30/01/2016 : Substitution. Mise en forme clausale. Problème SAT. Algorithme de Quine pour la satisfaisabilité.
  4. 6/02/2017 : Algorithme DPLL pour la satisfaisabilité. Notion de système de preuve. La méthode de la coupure (résolution propositionnelle). Correction de la méthode. Complètude de la méthode de la coupure.
  5. 13/02/2017 : Complètude de la méthode de la coupure. Syntaxe de la logique du premier ordre : signature, langage, termes, formules atomiques, formules; variables libres et liées. Sémantique : structure pour un langage, valuations, évaluation des termes, évaluation des formules atomiques.
  6. 27/02/2017 : Évaluation des toutes les formules. Notions de modèle, tautologie, conséquece logique, équivalence logique. Équivalences classiques avec les quantificateurs.
  7. 6/03/2017 : Forme prénexe, Skolemisation, forme clausale. Clauses, au premier ordre. Unification. Termes, substitutions, problèmes d'unification, unificateurs, MGUs.
  8. 13/03/2017 : Algorithme d'unification. Calcul de la résolution. Correction et complétude du calcul. Indecidabilité de la logique du premier ordre.

Documents du cours

Par ici.

En TP

Enoncés des TPs : TP1, TP2, TP3, TP4.

Références

Des démos

Autres lectures conseillées

Se preparer à l'examen

Les annales des examens passés sont disponibles ici.

Calcul de la note finale

NF = MAX (0.33*CC + 0.67*ET ; ET)
Attention : aucun document n'est authorisé à l'examen.