diff options
Diffstat (limited to 'programme-inf110.tex')
| -rw-r--r-- | programme-inf110.tex | 14 |
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$. |