Logique et Calculabilité (2015)


Infos

Emploi du temps

Le calendrier sciences de AMU.
Organisation du cours : 2h *10 cours, 3h*10 TDs, 2h*5 TPs.
  1. 19/01/2015 : 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. 26/01/2015 : Conséquence logique d'un ensemble de formules. Propriétés de la conséquence logique. Théorème de compacité.
  3. 2/02/2015 : Équivalences élémentaires entre formules. Substitution. Mise en forme clausale. Problème SAT. Méthode de Quine pour la satisfaisabilité.
  4. 9/02/2015 : 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. 16/02/2015 : Syntaxe de la logique du premier ordre : signature, langage, termes, formules atomiques, formules; variables libtres et liées. Sémantique : structure pour un langage.
  6. 2/03/2015 : Sémantique de la logique du premier ordre : valuations, évaluation des termes, évaluation des formules atomiques, évaluations des formules. Notions de modèle, de de tautologie, conséquece logique, équivalence logique.
  7. 9/03/2015 : Équivalences classiques avec les quantificateurs. Forme prénexe, Skolemisation, forme clausale. Clauses, au premier ordre.
  8. 16/03/2015 : Unification. Termes, substitutions, problèmes d'unification, unificateurs et MGUs. Algorithme d'unification, terminaison, correction et complétude.
  9. 23/03/2015 : Calcul de la résolution. Correction et complétude du calcul.
  10. 30/03/2015 : Calculabilité. Machines de Turing, problèmes de décision, problèmes décidables, problèmes semi-décidables; le problème de l'arrêt, problème indécidable; thèse de Church.

En TP

Enoncés des TPs (depuis l'année dernière, susceptibles de modifications) : TP1, TP2, TP3, TP4, TP5.

Documents du cours

Par ici.

Références

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)