Logique et démonstration
Aperçu des sections
-
-
Ceci est la page du cours de logique, premier semestre de L1 maths-info. Vous y trouverez des supports de cours, les feuilles de TD et de TP, ainsi que des documents pour vous aider dans votre apprentissage et vos révisions.
Pour toute question relative au cours, contactez le responsable du module par mail : Jules Chouquet (prenom.nom@univ-orleans.fr)
-
-
Le module est évalué en contrôle continu. Il y aura des contrôles écrits courts en fin de certaines séances de TD (à partir de la semaine du 9 octobre, toutes les deux semaines), en un dernier en fin de séance de TP. Les contrôles porteront sur tout ce qui aura été vu en cours et en TD jusqu’à la semaine précédente. (le contrôle ne demandera pas quelque chose vu la semaine en cours).
La répartition est la suivante : les 4 notes obtenues en contrôle pendant le semestre donneront une moyenne valant pour 60% de la note finale du module. Il y aura un partiel en fin de semestre, valant 40% de la note finale.
-
-
Vous trouverez dans cette section des tutos pour vous familiariser avec Coq.
Pour les essayer, vous pouvez installer Coq-Platform sur votre machine personnelle, c’est ce que nous utiliserons en TP (l’interface utilisateur s’appelle CoqIDE).
Mais vous pouvez également, si vous voulez juste faire quelques essais, utiliser un éditeur en ligne disponible à cette adresse. (il faut cliquer sur "scratchpad" pour commencer à coder).
ATTENTION : Dans les tutos, je vous indique les raccourcis claviers pour Coq Platform. Si vous utilisez l’éditeur en ligne, ils sont différents. En particulier, pour avancer dans les tactiques, il faut utiliser [Alt + ↓] et non pas [Ctrl + ↓], de même pour les autres raccourcis.
Pour commencer le TP1, il faut charger le fichier "exercices.v" dans un éditeur Coq (soit CoqIde, soit jsCoq, en ligne).
-
Correction en Vidéo :