Logique et Calculabilité (2017--2018)

Intervenants

Infos

• Vous pouvez trouver ici un programme démo de l'algorithme dúnification. Vous pouvez aussi executer le programme via web par ici.
• Vous pouvez trouver ici un programme/demo de l'algorithme de mise en forme clausale, executable par web par ici
• Vous pouvez trouver ici un programme pour executer l'algorithme DPLL. Vous pouvez aussi acceder au programme via web par ici.
• Le plan du site.

Emploi du temps

1. 23/01/2018 : 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. 30/01/2018 : Conséquence logique d'un ensemble de formules. Propriétés de la conséquence logique. Théorème de compacité.
3. 06/02/2018 : Équivalences élémentaires entre formules propositionnelles. Substitution. Mise en forme clausale. Problème SAT. Algorithme de Quine pour la satisfaisabilité. Algorithme DPLL pour la satisfaisabilité.
4. 13/02/2018 : Notion de système de preuve. La méthode de la coupure (résolution propositionnelle). Correction et complètude de cette méthode. Autres systèmes de preuve pour la logique propositionnelle.
5. 20/02/2018 : Complètude de la méthode de la coupure. Logique du premier ordre (calcul des prédicats). Syntaxe : signature, langage, termes, formules atomiques, formules; variables libres et liées.
6. 6/03/2018 : Sémantique : structure pour un langage, valuations, évaluation des termes, évaluation des formules atomiques, évaluation des formules. Notions de modèle, tautologie, conséquece logique, équivalence logique.
7. 13/03/2017 : Équivalences classiques avec les quantificateurs. Forme prénexe, Skolemisation, forme clausale. Clauses, au premier ordre.
8. 20/03/2018 : Unification. Termes, substitutions, problèmes d'unification, unificateurs, MGUs. Algorithme d'unification. Calcul de la résolution. Correction et complétude du calcul. Indecidabilité de la logique du premier ordre.
9. 27/03/2018 et 3/04/2018: Calculabilité. Lien vers la page de Kevin Perrot sur la calculabilité.

Documents du cours et code

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.

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.

Démos

• L'algorithme de mise en FNC.
• L'algorithme DPLL.
• L'algorithme d'unification.

Se preparer à l'examen

Calcul de la note finale