UE LIFLC: Logique classique, automne 2018

Page de LIFLF

Descriptif sur Offre de Formation

<note important> TP Noté du 10/12/2018

Unique document autorisé: liflc-2018a-coqnat.pdf

Lien vers le sujet de 10h00: LIFLC-TPNote-SujetA.v (actif à 10h)

Lien vers le sujet de 10h45: LIFLC-TPNote-SujetB.v (actif à 10h45) </note>

• Séance du 10/09/2018: diapositives
• Séances du 17/09/2018: diapositives, TD1+correction
• Séances du 24/09/2018: diapositives, TD2+correction
• Séances du 01/10/2018: diapositives, code, TD3+correction
• Séances du 08/10/2018: TP1 (correction), Lien Coq - Déduction Naturelle, TD4+correction
• Séances du 15/10/2018: TP2 (correction)
• Contrôle le lundi 22/10/2018, annale 2017
• Séance du 6/11: diapositives
• Séances du 12/11: diapositives, TD5+correction
• Séances du 19/11: TP3, (correction) (jusqu'à F inclus), TD6+correction.
• Séances du 26/11: TP4, (correction).
• Séance du 3/12: diapositives, TD7+correction, sémantique Imp.
• Séance du 10/12: TP Noté (sujet d'entrainement)

• Petit guide de survie en Coq
• Cheatsheet
• Documentations officielle de Coq

Emploi du temps complet, semaine courante

• Séance du 11/09/2017: diapositives
• Séance du 18/09/2017: diapositives
• Séance du 25/09/2017: diapositives
• Séance du 02/10/2017: diapositives
• Séance du 06/11/2017: diapositives
• Séance du 13/11/2017: diapositives
• Séance du 27/11/2017 diapositives + extrait Coq de Software Foundations

• Lundi 18/09/2017: TD1+correction
• Lundi 25/09/2017: TD2+correction (mise-à-jour exercice 4 wrt la feuille distribuée en TD)
• Lundi 02/10/2017: TD3+correction
• Lundi 09/10/2017: TP1: prise en main de Coq (correction), lien avec la déduction naturelle, TD4+correction
• Lundi 16/10/2017: TP2: listes et induction (finir les exercices 1&2 du TP1 avant de commencer le TP2)
• Lundi 13/11/2017: TD6+correction partielle
• Lundi 20/11/2017: reprendre et terminer le TP2
• Lundi 27/11/2017: TP3 + finir le TP2 si ce n'est pas fait
• Lundi 4/12/2017: TD7

Emploi du temps complet, semaine courante

Groupe A: Sylvain BRANDEL, Emploi du temps

Groupe B: Emmanuel COQUERY, Emploi du temps

Groupe C: Romuald THION, Emploi du temps

Groupe D: Xavier URBAIN, Emploi du temps

Groupe E: Ugo COMIGNANI, Emploi du temps

1. Mémo syntaxe et sémantique du calcul propositionnel, substitutions (maj le 09/09/2014)
2. Mémo systèmes de déduction syntaxiques (maj le 26/09/2013)
3. Mémo calcul de séquent en calcul propositionnel (maj le 04/11/2013)
4. Mémo sur SAT et DPLL
5. Mémo sur la syntaxe et la sémantique du calcul de prédicats
6. Mémo sur la résolution au premier ordre

Mémo résolution en calcul propositionnel Ancien programme, pour archives.

• TD1 (19/09/2016), correction
• TD2 (26/09/2016), correction
• TD3 (03/10/2016), correction
• TD4, correction
• TD5, correction

Voir le sujet ici.

Le sujet est également disponible dans l'archive fournie et sur un dépôt de la forge (hg pull https://forge.univ-lyon1.fr/hg/inf3034l-liflc-projet-2016).

• Contrôle à mi-parcours le lundi 17 octobre 2016 à 9h45 → 11% 16% (1/6^eme)
• Projet à rendre pour le 18 décembre 2016 → 22% 16% (1/6^eme)
• Épreuve finale → 67% (2/3)

Emploi du temps complet, semaine courante

Emploi du temps du groupe A

Emploi du temps du groupe B

Emploi du temps du groupe C

Emploi du temps du groupe D

Emploi du temps du groupe E

• Énoncé contrôle terminal 2008-2009
• Énoncé contrôle terminal 2009-2010
• Énoncé contrôle terminal 2010-2011
• Énoncé contrôle terminal 2011-2012
• Énoncé contrôle terminal 2012-2013
• Énoncé contrôle terminal 2013-2014
• Énoncé contrôle terminal 2014-2015
• Contrôle 1 corrigé 2015-2016
• Contrôle 2 corrigé 2015-2016
• Énoncé contrôle terminal 2015-2016
• Énoncé de l'examen 2016-2017, première session
• Énoncé de l'examen 2017-2018, première session

• Jean Gallier: Logic for Computer Science: Foundations of Automatic Theorem Proving.