Logique et Calculabilité (2015)
Infos
- Le 9 février, le cours aura lieu en amphi Perez
- Début du cours : le lundi 19/01/2015 (salle LSH 401).
- Début des TDs : le lundi 26/01/2015 (salles BU2 et BU3, voir le
plan
du site).
- Début des TPs : le lundi 2/03/2015.
Emploi du temps
Le
calendrier
sciences de AMU.
Organisation du cours : 2h *10 cours, 3h*10 TDs, 2h*5 TPs.
- 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.
- 26/01/2015 : Conséquence logique d'un ensemble de
formules. Propriétés de la conséquence logique. Théorème de
compacité.
- 2/02/2015 : Équivalences élémentaires entre formules. Substitution. Mise en forme clausale. Problème SAT. Méthode de Quine pour la satisfaisabilité.
- 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.
- 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.
- 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.
- 9/03/2015 : Équivalences classiques avec les
quantificateurs. Forme prénexe, Skolemisation, forme clausale.
Clauses, au premier ordre.
- 16/03/2015 : Unification. Termes, substitutions, problèmes
d'unification, unificateurs et MGUs. Algorithme d'unification,
terminaison, correction et complétude.
- 23/03/2015 : Calcul de la résolution. Correction et complétude du calcul.
- 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
- Manuel
de Prover9
et Mace4
- Pour utiliser Prover9 er Mace4 via l'interface graphique :
lancer la commande
python /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.
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
- 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
Les annales des examens passés sont
disponibles ici.
Calcul de la note finale
NF = MAX (0.33*CC + 0.67*ET ; ET)