====== 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 =====

<note important>
**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)
</note>


==== 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}}

<del>{{:enseignement:logique:logique-memo4.pdf|Mémo résolution en calcul propositionnel}}</del> 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 ===

<del>Voir [[http://liris.cnrs.fr/~ecoquery/tps/liflc/2016/SUJET.html|le sujet ici]].</del>

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 -> <del>11%</del> 16% (1/6<sup>eme</sup>)
  * Projet à rendre pour le 18 décembre 2016 -> <del>22%</del> 16% (1/6<sup>eme</sup>)
  * É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]]//.