Logique et Calculabilité

Infos

• Attention : changement de salle pour le TD du vendredi 21/02/2014 : on se retrouve en Amphi Lavoisier.
• Début des TPs : le vendredi 21/02/2014, salle 302 8h00 et 14h00.
• Le premier CC aura lieu le vendredi 31/01.
• Le TD (un seul) a lieu en salle LSH 203.
• Début des TDs : le vendredi 24/01/2014.
• Début du cours : le mercredi 15/01/2014.

Emploi du temps

• 15/01. 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.
• 22/01. Modèles d'un ensemble de formules, conséquence logique d'un ensemble de formules. Théorème de compacité pour le calcul propositionnel (avec Lemme de König).
• 29/01. Équivalences élémentaires entre formules. Substitution. Mise en forme clausale. Problème SAT. Méthode de Quine pour la satisfaisabilité.
• 5/02. Algorithme DPLL pour la satisfaisabilité. Notion de système formel. La méthode de la coupure (résolution propositionnelle). Correction de la méthode.
• 12/02. Completude de la méthode de la coupure. Logique du premier ordre : syntaxe.
• 19/02. Logique du premier ordre, sémantique (structure pour un langage, valuations, évaluation des termes, évaluation des formules atomiques, évaluations des formules).
• 5/03. Logique du premier ordre : notions d'équivalence, de tautologie, de modèle ; équivalences classiques avec les quantificateurs ; mise en forme prénexe.
• 12/03. Logique du premier ordre. Skolemisation, forme normale conjonctive. Termes, substitutions, problèmes d'unification. Algorithme d'unification.
• 19/03. Unification. Calcul de la résolution. Correction et complétude du calcul.
• 26/03. 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

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

Documents du cours

Références

• Les notes du cours, disponibles ici au fur et à mesure.

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