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 (environ 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).
Les absences non justifiées à ces évaluations sont bien sûr rédhibitoires pour valider le module.
Les étudiants en Régime Spécial d’Études auront un examen unique d’1h30 (2h si tiers temps)
En deuxième session, ce sera également un examen d’1h30 (2h si tiers temps).
-
-
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 :
Lecteur vidéo is loading.