the end

src/bdd.tex

@@ -65,7 +65,7 @@
 
       Ce qui se lit: \enquote{Si $P$, alors, $Q_1$, sinon, $Q_2$.}.
     \subsubsection{Forme normale \texttt{if-then-else}}
-    On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable. On recommande la lecture de \cite{} au lecture curieux d'en apprendre plus à ce sujet.
+    On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable. On recommande la lecture de \cite{Mohring93} au lecteur curieux d'en apprendre plus à ce sujet.
     \subsubsection{Expansion de \bsc{Shannon}}
       On note $P[Q_1/Q_2]$  la proposition $P$ dans laquelle on a substitué toutes les occurences de $Q_1$ par $Q_2$. On a alors:
         \[P = Q \rightarrow P[Q/\top], P[Q/\bot]\]

src/bib.bib

@@ -20,6 +20,25 @@ verification, symbolic manipulation, symbolic manipulation, Boolean
 functions, binary decision diagrams, logic design verification},
 }
 
+@article{Mohring93,
+ author = {Paulin-Mohring, Christine and Werner, Benjamin},
+ title = {Synthesis of ML Programs in the System Coq},
+ journal = {J. Symb. Comput.},
+ issue_date = {May/June 1993},
+ volume = {15},
+ number = {5-6},
+ month = may,
+ year = {1993},
+ issn = {0747-7171},
+ pages = {607--640},
+ numpages = {34},
+ url = {http://dx.doi.org/10.1016/S0747-7171(06)80007-6},
+ doi = {10.1016/S0747-7171(06)80007-6},
+ acmid = {162217},
+ publisher = {Academic Press, Inc.},
+ address = {Duluth, MN, USA},
+}
+
 @misc{Andersen97,
   author = {Henrik Reif Andersen},
   title = {An Introduction to Binary Decision Diagrams},