====== UE LIFLC: Logique classique, automne 2018 ======
[[http://liris.cnrs.fr/sylvain.brandel/wiki/doku.php?id=ens:liflf|Page de LIFLF]]
[[http://offre-de-formations.univ-lyon1.fr/ue-12086-12/logique-classique.html|Descriptif sur Offre de Formation]]
===== Année 2018-2019 =====
**TP Noté du 10/12/2018**
Unique document autorisé: {{ :enseignement:logique:liflc-2018a-coqnat.pdf |}}
Lien vers le sujet de 10h00: [[https://perso.liris.cnrs.fr/ecoquery/enseignement/liflc/LIFLC-TPNote-SujetA.v|LIFLC-TPNote-SujetA.v]] (actif à 10h)
Lien vers le sujet de 10h45: [[https://perso.liris.cnrs.fr/ecoquery/enseignement/liflc/LIFLC-TPNote-SujetB.v|LIFLC-TPNote-SujetB.v]] (actif à 10h45)
==== Supports ====
* Séance du 10/09/2018: {{ :enseignement:logique:liflc-2018a-cm1.pdf |diapositives}}
* Séances du 17/09/2018: {{ :enseignement:logique:liflc-2018a-cm2.pdf |diapositives}}, {{ :enseignement:logique:liflc-2018a-td1-correction.pdf |TD1+correction}}
* Séances du 24/09/2018: {{ :enseignement:logique:liflc-2018a-cm3.pdf |diapositives}}, {{ :enseignement:logique:liflc-2018a-td2-correction.pdf |TD2+correction}}
* Séances du 01/10/2018: {{ :enseignement:logique:liflc-2018a-cm4.pdf |diapositives}}, code, {{ :enseignement:logique:liflc-2018a-td3-correction.pdf |TD3+correction}}
* Séances du 08/10/2018: [[https://perso.liris.cnrs.fr/ecoquery/enseignement/liflc/LIFLC-TP1.v|TP1]] ([[https://perso.liris.cnrs.fr/ecoquery/enseignement/liflc/LIFLC-TP1-correction.v|correction]]), {{ :enseignement:logique:liflc-2018a-coqnat.pdf |Lien Coq - Déduction Naturelle}}, {{ :enseignement:logique:liflc-2018a-td4-correction.pdf |TD4+correction}}
* Séances du 15/10/2018: [[https://perso.liris.cnrs.fr/ecoquery/enseignement/liflc/LIFLC-TP2.v|TP2]] ([[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TP2-correction.v|correction]])
* Contrôle le lundi 22/10/2018, {{ :enseignement:logique:liflc-2017a-partiel.pdf |annale 2017}}
* Séance du 6/11: {{ :enseignement:logique:liflc-2018a-cm5.pdf |diapositives}}
* Séances du 12/11: {{ :enseignement:logique:liflc-2018a-cm6.pdf |diapositives}}, {{ :enseignement:logique:liflc-2018a-td5-correction.pdf |TD5+correction}}
* Séances du 19/11: [[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TP3.v|TP3]], ([[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TP3-correction.v|correction]]) (jusqu'à F inclus), {{ :enseignement:logique:liflc-2018a-td6-correction.pdf |TD6+correction}}.
* Séances du 26/11: [[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TP4.v|TP4]], ([[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TP4-correction.v|correction]]).
* Séance du 3/12: {{ :enseignement:logique:liflc-2018a-cm8.pdf |diapositives}}, {{ :enseignement:logique:liflc-2018a-td7-correction.pdf |TD7+correction}}, {{ :enseignement:logique:sem-imp.pdf |sémantique Imp}}.
* Séance du 10/12: TP Noté ([[https://perso.liris.cnrs.fr/emmanuel.coquery/enseignement/liflc/LIFLC-TPNote-SujetC.v|sujet d'entrainement]])
=== Liens Coq ===
* [[http://lim.univ-reunion.fr/staff/fred/Enseignement/IntroCoq/Exos-Coq/Petit-guide-de-survie-en-Coq.html|Petit guide de survie en Coq]]
* [[http://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf|Cheatsheet]]
* [[https://coq.inria.fr/refman/|Documentations officielle de Coq]]
==== Organisation ====
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28317,28318,28319,28321,28322,28323,28325,28326,28327,28329,28330,28331,28337,28339,28340,28342,28343,28344|Emploi du temps complet, semaine courante]]
|Groupe|Intervenant-e|Emploi du temps|
|A|Sylvain Brandel| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28317,28318,28319|ADE]]|
|B|Emmanuel Coquery| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28321,28322,28323|ADE]]|
|C|Romuald Thion| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28325,28326,28327|ADE]]|
|D|Xavier Urbain| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28329,28330,28331|ADE]]|
|E|Laure Gonnord| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28337,28339,28340|ADE]]|
|F|Nicolas Louvet| [[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=2&days=0,1,2,3,4&ShowPianoWeeks=true&showTree=true&resources=28342,28343,28344|ADE]]|
----
===== Année 2017-2018 =====
==== Diapositives ====
* Séance du 11/09/2017: {{:enseignement:logique:liflc-2017a-cm1.pdf |diapositives}}
* Séance du 18/09/2017: {{ :enseignement:logique:liflc-2017a-cm2.pdf |diapositives}}
* Séance du 25/09/2017: {{ :enseignement:logique:liflc-2017a-cm3.pdf |diapositives}}
* Séance du 02/10/2017: {{ :enseignement:logique:liflc-2017a-cm4.pdf |diapositives}}
* Séance du 06/11/2017: {{ :enseignement:logique:liflc-2017a-cm5.pdf |diapositives}}
* Séance du 13/11/2017: {{ :enseignement:logique:liflc-2017a-cm6.pdf |diapositives}}
* Séance du 27/11/2017 {{ :enseignement:logique:liflc-2017a-cm7.pdf |diapositives}} + [[https://liris.cnrs.fr/~ecoquery/enseignement/liflc/CM7.v|extrait Coq]] de [[https://softwarefoundations.cis.upenn.edu/|Software Foundations]]
==== Sujets de TD/TP ====
* Lundi 18/09/2017: {{ :enseignement:logique:liflc-2017a-td1-correction.pdf |TD1+correction}}
* Lundi 25/09/2017: {{ :enseignement:logique:liflc-2017a-td2-correction.pdf |TD2+correction}} (mise-à-jour exercice 4 wrt la feuille distribuée en TD)
* Lundi 02/10/2017: {{ :enseignement:logique:liflc-2017a-td3-correction.pdf |TD3+correction}}
* Lundi 09/10/2017: [[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-2017A-TP1.html|TP1: prise en main de Coq]] ([[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-TP1-correction.v|correction]]), {{ :enseignement:logique:liflc-2017a-coqnat.pdf |lien avec la déduction naturelle}}, {{ :enseignement:logique:liflc-2017a-td4-correction.pdf |TD4+correction}}
* Lundi 16/10/2017: [[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-2017A-TP2.html|TP2: listes et induction]] (finir les exercices 1&2 du TP1 avant de commencer le TP2)
* Lundi 13/11/2017: {{ :enseignement:logique:liflc-2017a-td6-correction.pdf |TD6+correction partielle}}
* Lundi 20/11/2017: reprendre et terminer le [[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-2017A-TP2.html|TP2]]
* Lundi 27/11/2017: [[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-2017A-TP3.html|TP3]] + finir le [[http://liris.cnrs.fr/~ecoquery/enseignement/liflc/LIFLC-2017A-TP2.html|TP2]] si ce n'est pas fait
* Lundi 4/12/2017: {{ :enseignement:logique:liflc-2017a-td7.pdf |TD7}}
==== Organisation ====
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28317,28318,28319,28321,28322,28323,28325,28326,28327,28329,28330,28331,28337,28339,28340&displayConfName=DOUA_SCIENCES&days=0&weeks=&showTree=false|Emploi du temps complet, semaine courante]]
Groupe A: Sylvain BRANDEL,
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28317,28318,28319&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps]]
Groupe B: Emmanuel COQUERY,
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28321,28322,28323&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps]]
Groupe C: Romuald THION,
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28325,28326,28327&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps]]
Groupe D: Xavier URBAIN,
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28329,28330,28331&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps]]
Groupe E: Ugo COMIGNANI,
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=1&ShowPianoWeeks=true&resources=28337,28339,28340&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps]]
----------
===== Année 2016 =====
=== Mémos ===
- {{:enseignement:logique:logique-memo1.pdf|Mémo syntaxe et sémantique du calcul propositionnel, substitutions}} (maj le 09/09/2014)
- {{:enseignement:logique:logique-memo2.pdf|Mémo systèmes de déduction syntaxiques}} (maj le 26/09/2013)
- {{:enseignement:logique:logique-memo3.pdf|Mémo calcul de séquent en calcul propositionnel}} (maj le 04/11/2013)
- {{:enseignement:logique:logique-memo-sat.pdf|Mémo sur SAT et DPLL}}
- {{:enseignement:logique:logique-memo5.pdf|Mémo sur la syntaxe et la sémantique du calcul de prédicats}}
- {{:enseignement:logique:logique-memo6.pdf|Mémo sur la résolution au premier ordre}}
{{:enseignement:logique:logique-memo4.pdf|Mémo résolution en calcul propositionnel}} Ancien programme, pour archives.
=== TD ===
* {{:enseignement:logique:logique-td1-enonce.pdf|TD1}} (19/09/2016), {{:enseignement:logique:logique-td1-correction.pdf|correction}}
* {{:enseignement:logique:logique-td2-enonce.pdf|TD2}} (26/09/2016), {{:enseignement:logique:logique-td2-correction.pdf|correction}}
* {{:enseignement:logique:logique-td3-enonce.pdf|TD3}} (03/10/2016), {{:enseignement:logique:logique-td3-correction.pdf|correction}}
* {{ :enseignement:logique:logique-td4-enonce.pdf |TD4}}, {{ :enseignement:logique:logique-td4-correction.pdf |correction}}
* {{ :enseignement:logique:logique-td5-enonce.pdf |TD5}}, {{ :enseignement:logique:logique-td5-correction.pdf |correction}}
=== Projet ===
Voir [[http://liris.cnrs.fr/~ecoquery/tps/liflc/2016/SUJET.html|le sujet ici]].
Le sujet est également disponible dans [[http://liris.cnrs.fr/~ecoquery/files/inf3034l-liflc-projet-2016.zip|l'archive fournie]] et sur un dépôt de la forge (''hg pull https://forge.univ-lyon1.fr/hg/inf3034l-liflc-projet-2016'').
=== Evaluation ===
* Contrôle à mi-parcours le lundi 17 octobre 2016 à 9h45 -> 11% 16% (1/6eme)
* Projet à rendre pour le 18 décembre 2016 -> 22% 16% (1/6eme)
* Épreuve finale -> 67% (2/3)
=== Emploi du temps ===
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28317,28318,28319,28321,28322,28323,28325,28326,28327,28329,28330,28331,28337,28339,28340&displayConfName=DOUA_SCIENCES&days=0&weeks=&showTree=false|Emploi du temps complet, semaine courante]]
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28317,28318,28319&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps du groupe A]]
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28321,28322,28323&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps du groupe B]]
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28325,28326,28327&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps du groupe C]]
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28329,28330,28331&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps du groupe D]]
[[http://adelb.univ-lyon1.fr/direct/index.jsp?projectId=3&ShowPianoWeeks=true&resources=28337,28339,28340&displayConfName=DOUA_SCIENCES&days=0&weeks=4,5,6,7,8,9,10,11,12,13,14,15,16,17&showTree=false|Emploi du temps du groupe E]]
===== Annales ======
* {{:enseignement:logique:lif11-cct-2008.pdf|Énoncé contrôle terminal 2008-2009}}
* {{:enseignement:logique:lif11-cct-2009.pdf|Énoncé contrôle terminal 2009-2010}}
* {{:enseignement:logique:lif11-2010-ccf.pdf|Énoncé contrôle terminal 2010-2011}}
* {{:enseignement:logique:lif11-2011-ccf.pdf|Énoncé contrôle terminal 2011-2012}}
* {{:enseignement:logique:lif11-2012-ccf.pdf|Énoncé contrôle terminal 2012-2013}}
* {{:enseignement:logique:lif11-2013-ccf.pdf|Énoncé contrôle terminal 2013-2014}}
* {{:enseignement:logique:lif11-2014-ccf.pdf|Énoncé contrôle terminal 2014-2015}}
* {{:enseignement:logique:lif11_2015-2016_cc1_correction.pdf|Contrôle 1 corrigé 2015-2016}}
* {{:enseignement:logique:lif11_2015-2016_cc2_correction.pdf|Contrôle 2 corrigé 2015-2016}}
* {{:enseignement:logique:lif11-2015-ccf.pdf|Énoncé contrôle terminal 2015-2016}}
* {{ :enseignement:logique:liflc-examen-2016-2017-s1.pdf |Énoncé de l'examen 2016-2017, première session}}
* {{ :enseignement:logique:liflc-examen-2017-2018-s1.pdf |Énoncé de l'examen 2017-2018, première session}}
===== Références =====
* Jean Gallier: //[[http://www.cis.upenn.edu/~jean/gbooks/logic.html|Logic for Computer Science:
Foundations of Automatic Theorem Proving]]//.