A few clarifications on the syllabus.

1 files changed, 7 insertions, 7 deletions

diff --git a/programme-inf110.tex b/programme-inf110.tex
index 85ea37f..ff5bb1c 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -98,11 +98,11 @@ Git: \input{vcline.tex}
 \item \textbf{Arithmétique du premier ordre :} les axiomes de Peano ;
   l'idée générale que Curry-Howard sur l'arithmétique de Heyting
   permet d'extraire des algorithmes des preuves ; le fait qu'il est
-  possible formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
-  Heyting/Peano ; le fait que vérifier si une preuve est valable est
-  décidable, mais que savoir si un énoncé est un théorème est
-  seulement semi-décidable ; l'énoncé du théorème de Gödel et l'idée
-  de sa démonstration.
+  possible de formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
+  Heyting/Peano (sans détails) ; le fait que vérifier si une preuve
+  est valable est décidable, mais que savoir si un énoncé est un
+  théorème est seulement semi-décidable ; l'énoncé du théorème de
+  Gödel et l'idée de sa démonstration.
 \item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée
   en TP, et notamment les principales tactiques de raisonnement (sur
   les connecteurs logiques, types inductifs, égalités, etc.).  Le nom
@@ -138,8 +138,8 @@ Git: \input{vcline.tex}
   $\lambda\mu$-calcul.
 \item Les subtilités de la réalisabilité propositionnelle (p.ex., la
   réalisabilité de la formule de Tseitin).  La sémantique des
-  problèmes finis n'est pas exigible (mais pourra être utilisée si on
-  le souhaite).
+  problèmes finis n'est pas non plus exigible (mais pourra être
+  utilisée si on le souhaite).
 \item Le $\lambda$-cube de Barendregt, les subtilités de la différence
   entre $\exists$ et types sommes, la notion de
   prédicativité/imprédicativité, le système $F$.