Logique et Calculabilité (2017)

Intervenants

Infos

• Vous pouvez trouver ici un programme pour executer l'algorithme DPLL. Vous pouvez aussi acceder au programme via web par ici.
• Attention : possible déplacement des cours et des TDS de LSH vers le batiment 5.
• Début du cours : le lundi 16/01/2017 à 15h00 (salle LSH 501).
• Début des TDs : le lundi 23/01/2016 à 9h00 (salles LSH 412 et 205, voir le plan du site).

Emploi du temps

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

En TP

• Manuel de Prover9 et Mace4
• Pour utiliser Prover9 er Mace4 via l'interface graphique : lancer la commande prover9-mace4-gui depuis un terminal.
• Des outils pour visualiser les preuves et les modèles, on les trouve par ici.

Références

• Les notes du cours, disponibles ici au fur et à mesure.
• Page web du cours de l'année dernière ici.

Des démos

• L'algorithme DPLL.

Autres lectures conseillées

• Le livre Logique mathématique 1 (calcul propositionnel ; algèbre de Boole ; calcul des prédicats) par René Cori et Daniel Lascar.

Se preparer à l'examen

Calcul de la note finale