\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  %article,%    Pour sortir le support du cours
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage{%
%  t1enc,
  fancybox%             Les boites
  }
\usepackage{color}
\usepackage[dvips]{graphicx}

\usepackage{stmaryrd,amssymb}
\usepackage{prooftree}
\usepackage[all]{xy}
\usepackage{qsymbols}

\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips

\slidesmag{5}
\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*


\title{\emph{La logique de la connaissance}}

\author{}

\date{}

\newcommand{\logoLIP}{\includegraphics*[height=0.04\textwidth]{lipllipl.eps}}
\newcommand{\logoENS}{\includegraphics*[height=0.04\textwidth]{liplensl.eps}}
\newcommand{\logos}{\hspace*{6pt}MIM-1 ---Cours de Logique --- Automne 2002 \hfill\logoENS}

\newpagestyle{AvecLogos}%
  {%\tiny \em WADT'95 -- \jour 
  \hfil \thepage} % \rightmark
  {\logos}
\pagestyle{AvecLogos}

%\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   

\definecolor{mauve}{rgb}{1,0,1}
\definecolor{cyanp}{rgb}{0,1,1}
\renewcommand{\emph}[1]{{\color{red}#1}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\newcommand{\ud}[1]{\underline{#1}}
\renewcommand{\phi}{\varphi}
\newcommand{\force}{\mathop{\textsf{\large I}\!\!\vdash}}

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\newcommand{\heading}[1]{%
{\color{mauve}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}

\CompileMatrices

\maketitle                      % en mode article

\begin{slide}
  \ifslidesonly              % Title slide only for slidesonly selection.
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}
  \fi
\end{slide}

\begin{slide}
\heading{Un protocole émetteur-récepteur}
Les noeuds $\bigcirc$ transmettent les messages entre l'émetteur et le
récepteur:
\begin{itemize}
\item ils \emph{ peuvent dupliquer} des messages,

\item ils \emph{peuvent perdre} des messages,
  
\item cependant, ils ne peuvent pas \emph{perdre indéfiniment } un même
  message.
\end{itemize}

C'est le principe d'\textbf{Internet}~: \emph{«faire de son mieux»} (en anglais
\emph{«the best effort»}).  Le protocole s'appelle \textbf{TCP} (pour
\emph{Transmission Control Protocol}).
\end{slide}
%------------------------------------------------------
\begin{slide}
%
%%%%%%%%%%%%%%
\begin{center}
\includegraphics[width=4cm]{emet-recep.eps} %\hfill
\end{center}
%%%%%%%%%%%%%%
%
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un protocole émetteur-récepteur \textit{(suite)}}

Tant que l'émetteur \emph{\textbf{ne sait pas}} si le récepteur a reçu
un message donné $m_i$, il le ré-émet.  

Le récepteur accuse réception d'un message en émettant un message
d'\emph{accusé réception} $ack_i$ tant qu'il \emph{\textbf{ne sait pas}} si
l'émetteur a reçu cet accusé réception.

%On peut «montrer» que 

%\fbox{\emph{tous les messages seront tôt ou tard reçus,
%  dans l'ordre de leur émission.}}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'attaque coordonnée}

\begin{itemize}
\item Deux généraux et leurs armées sur deux collines,
  
\item Ils doivent attaquer \emph{ensemble} et chaque général doit être sûr
  que l'autre général attaquera en même temps.

\item \emph{Ils communiquent par des messagers}

  \begin{itemize}
  \item qui mettent une heure pour aller d'un camp à l'autre,
  \item qui peuvent se perdre dans le noir ou être capturés.
  \end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'attaque coordonnée}

\begin{itemize}
\item Deux généraux et leurs armées sur deux collines,
  
\item Ils doivent attaquer \emph{ensemble} et chaque général doit être sûr
  que l'autre général attaquera en même temps.

\item \emph{Ils communiquent par des messagers}

  \begin{itemize}
  \item qui mettent une heure pour aller d'un camp à l'autre,
  \item qui peuvent se perdre dans le noir ou être capturés.
  \end{itemize}
\end{itemize}
\emph{Comment coordonner une attaque?}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
%%%%%%%%%%%%%%
\begin{center}
\includegraphics[width=4.5cm]{2generaux.eps} %\hfill
\end{center}
%%%%%%%%%%%%%%
%
\end{slide}
\begin{slide}
  \heading{La sécurité sur Internet} 
  
  Transformer des \emph{«\textbf{je crois que}»} en \emph{«\textbf{je
      sais que}»}.

Les messages circulent le réseau public que façon codée, mais ça n'est 
pas suffisant.

Des intrus sur le réseau, écoutent les messages, les stockent et
fabriquent de faux messages.

\bleu{A} a reçu un message de \bleu{B}, \bleu{A} doit pouvoir affirmer
\textit{«\emph{\textbf{Je sais que}} le message que j'ai reçu a bien
  été émis par \bleu{B}».  }
\end{slide}
%%------------------------------------------------------
%\begin{slide}
%\heading{Protocoles cryptographiques}


%$\textbf{messages}\left\{\begin{array}{ll}
%\textit{confidentialité} & 
%\begin{footnotesize}
%  \textrm{(codage robuste et absence de fuite d'information),}
%\end{footnotesize}
%\\
%\textit{intégrité}, &\\
%\end{array}
%\right.$

%\textbf{agents} \hspace*{24pt}\textit{authentification},

%\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{mauve}{\textit{Jouons un peu}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les as et les huit}

Il y a huit cartes : \bl{quatre as} et \bl{quatre 8}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les as et les huit}

Il y a huit cartes : \bl{quatre as} et \bl{quatre 8}.

Chaque joueur reçoit deux cartes qu'il ne regarde pas, \ali mais
qu'il montre à tout le monde.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les as et les huit}

Il y a huit cartes : \bl{quatre as} et \bl{quatre 8}.

Chaque joueur reçoit deux cartes qu'il ne regarde pas, \ali mais
qu'il montre à tout le monde.

Chaque joueur parle à son tour:
\begin{itemize}
\item Soit il dit \emph{Je ne sais pas},
\item Soit il dit 
  \begin{itemize}
  \item \emph{J'ai deux as},
  \item \emph{J'ai deux 8},
  \item \emph{J'ai un as et un huit}.
  \end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les as et les huit}

On fait autant de tours qu'il faut.

Il y a \emph{toujours} un joueur qui peut deviner les cartes qu'il a. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les as et les huit}

On fait autant de tours qu'il faut.

Il y a \emph{toujours} un joueur qui peut deviner les cartes qu'il a. 

\vspace*{20pt}

\begin{center}
\begin{LARGE}
 \VERT{ Comment cela se peut-il?}
\end{LARGE}

\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Monsieur \textit{Produit} et Monsieur \textit{Somme}}

Étant donnés deux nombres entre $2$ et $20$.  
\begin{itemize}
\item Monsieur \textit{Produit} connaît le produit de ces deux
  nombres,
  
\item et Monsieur \textit{Somme} connaît la somme de ces deux nombres.
\end{itemize}
\begin{description}
\item[\it Monsieur Produit:] - Je ne connais pas les deux nombres.
\item[\it Monsieur Somme~:] - Je le sais.
\item[\it Monsieur Produit~:] - Alors je connais les deux nombres.
\item[\it Monsieur Somme~:] - Alors, moi aussi je connais les deux nombres.
\end{description}
\end{slide}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les modalités}
Une modalité est un opérateur qui \emph{transforme} une sentence en une autre
sentence.

On crée un modalité \bleu{K_A} pour chaque agent \bleu{A}.

Une logique avec des modalités s'appelle la \emph{logique modale}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Qu'est-ce que la logique de la connaissance ?}
\begin{itemize}
\item La \VERT{logique de la connaissance} ou \VERT{logique
    épistémique} est la logique qui formalise
\begin{itemize}
\item ``\rouge{l'agent $i$ sait que $p$}'', noté \bleu{K_i(p)},
\item ``\rouge{$p$ est une connaissance commune}'', noté \bleu{C(p)}.
\end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La connaissance commune}
\bleu{C(p)} formalise des phrases comme
\begin{itemize}
\item \rouge{``C'est un fait bien connu que $p$, sauf des fous.''}
\item \rouge{``L'agent $i$ \VERT{sait que} l'agent $j$ \VERT{sait que} l'agent $i$
    \VERT{sait que} l'agent $j$ \VERT{sait que}, etc.''}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La connaissance commune}
\bleu{C(p)} formalise des phrases comme
\begin{itemize}
\item \rouge{``C'est un fait bien connu que $p$, sauf des fous.''}
\item \rouge{``L'agent $i$ \VERT{sait que} l'agent $j$ \VERT{sait que} l'agent $i$
    \VERT{sait que} , etc.''}.
\end{itemize}
On a besoin d'une modalité \bleu{E}, dite de ``connaissance partagée'', 
\rouge{``Tout le monde \VERT{sait que} $p$''},
\begin{color}{blue}
\[E_G(p) = \bigwedge_{i\in G} K_i(p).\]
\end{color}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La connaissance commune}
\bleu{C(p)} formalise des phrases comme
\begin{itemize}
\item \rouge{``C'est un fait bien connu que $p$, sauf des fous.''}
\item \rouge{``L'agent $i$ \VERT{sait que} l'agent $j$ \VERT{sait que} l'agent $i$
    \VERT{sait que} , etc.''}.
\end{itemize}
On a besoin d'une modalité \bleu{E}, dite de ``connaissance partagée'', 
\rouge{``Tout le monde \VERT{sait que} $p$''},
\begin{color}{blue}
\[E_G(p) = \bigwedge_{i\in G} K_i(p).\]
\end{color}

La \VERT{connaissance commune} \emph{n'est pas} la \VERT{connaissance
  partagée}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{mauve}{\textit{Les règles et les axiomes}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles}
C'est une logique qui se présente à la Hilbert.

\begin{displaymathbleu}
  \prooftree
  "|-" `f \qquad "|-" `f "=>" `j
  \justifies  "|-" `j
  \using \emph{(MP)}
  \endprooftree
\end{displaymathbleu}

La règle de généralisation de la connaissance
\begin{displaymathbleu}
  \prooftree
  "|-" `f
  \justifies"|-" K_i `f
  \using "|-" \emph{(GK)}
\endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les axiomes}
Il y \emph{tous les théorèmes de la logique classique propositionnelle
  classique}.
\begin{displaymathbleu}
  \prooftree
  \justifies "|-" `f
  \using \emph{(\textbf{Cl})} \qquad \textrm{\color{mauve} si \bleu{`f} est
    un théorème de la logique classique.}
  \endprooftree
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les axiomes}
Il y a quatre axiomes

L'\emph{axiome de distribution}
\begin{displaymathbleu}
  \prooftree
  \justifies "|-" K_i `f  "=>" K_i(`f "=>" `j) "=>"K_i `j
  \using \emph{(\textbf{K})}
  \endprooftree
\end{displaymathbleu}

L'\emph{axiome de la connaissance}
\begin{displaymathbleu}
  \prooftree
  \justifies "|-" K_i `f  "=>" `f
  \using \emph{(\textbf{T})}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les axiomes}

L'\emph{axiome d'introspection positive}
\begin{displaymathbleu}
  \prooftree
  \justifies "|-" K_i `f  "=>" K_i K_i `f
  \using \emph{(\textbf{4})}
  \endprooftree
\end{displaymathbleu}

L'\emph{axiome d'introspection négative}
\begin{displaymathbleu}
  \prooftree
  \justifies "|-" `! K_i `f  "=>" K_i `! K_i `f
  \using \emph{(\textbf{5})}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Attention}
En logique modale \emph{on n'a pas} la \emph{règle de déduction}

\textit{«De \bleu{G, `f "|-" `j} je déduis \bleu{G "|-"  `f "=>" `j}»}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les axiomes de la connaissance commune}%
Défintion de \bleu{E_G}
\begin{displaymathbleu}
  \prooftree
  \justifies"|-" E_G(`f) "<=>" \bigwedge_{i\in G} K_i(`f)
  \using \emph{(C1)}
  \endprooftree
\end{displaymathbleu}

\bleu{C_G `f} satisfait l'inégalité \bleu{`j "=>" E_G(`f \wedge `j)}.

\begin{displaymathbleu}
   \prooftree
  \justifies "|-" C_G `f "=>" E_G(`f \wedge C_G `f)
  \using \emph{(C2)}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles de la connaissance commune}%
\bleu{C_G `f} est le plus petit dans un certain sens, c'est-à-dire si
un \bleu{`j} satisfait \bleu{`j "=>" E_G(`f \wedge `j)} alors \bleu{`j
  "=>" C_G `f}.

\begin{displaymathbleu}
   \prooftree
   "|-" `j "=>" E_G(`j \wedge `f)
  \justifies "|-" `j "=>" C_G `f
  \using \emph{(RC1)}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{mauve}{\textit{Les modèles}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les modèles de Kripke}
On reprend des modèles de Kripke avec des relations d'équivalence.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un jeu très simple}

2 agents, 3 cartes \bleu{\{A, B, C\}}.

L'agent 1 reçoit une carte

L'agent 2 reçoit un carte

La troisième carte est retournée face contre la table/

Il y a six mondes possibles :
\ali \bleu{(A, B), (A,C), (B,A) (B, C), (C, A), (C, B)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un jeu très simple}%
  Dans le monde \bleu{(A,B)} l'agent \bleu{1} (sa relation
  d'accessibilité est noté par \xymatrix{\ar@{=}[r]&}) envisage deux
  mondes possibles à savoir \bleu{(A,B)} et \bleu{(A,C)}.
    \centerline{ 
    \xymatrix @C 16pt @R 12pt {
      & *++[o][F-]{A,B}  \ar@{=}[r] \ar@{-}[ld] \ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] %
          & *++[o][F-]{A,C} \ar@{-}[rd]\ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] \\
      *++[o][F-]{C,B} \ar@{=}[rd]\ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] %
          &&& *++[o][F-]{B,C} \ar@{=}[ld]\ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] \\
      & *++[o][F-]{C,A} \ar@{-}[r]\ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] %
          & *++[o][F-]{B, A} \ar@{=}@(ul,ur)[]\ar@{-}@(dl,dr)[] }}

\begin{center}
  Le modèle de Kripke \bleu{\mathcal{M}}.
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un jeu très simple} %
Les propositions primitives sont 
\begin{itemize}
\item \bleu{1A} le joueur (l'agent)  \bleu{1} détient la carte
  \bleu{A},
\item \bleu{2A} le joueur (l'agent)  \bleu{2} détient la carte
  \bleu{A},
\item \bleu{1B} le joueur (l'agent)  \bleu{1} détient la carte
  \bleu{B},
\item \bleu{2B} le joueur (l'agent)  \bleu{2} détient la carte
  \bleu{B},
\item \bleu{1C} le joueur (l'agent)  \bleu{1} détient la carte
  \bleu{C},
\item \bleu{2C} le joueur (l'agent)  \bleu{2} détient la carte
  \bleu{C}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Des assertions de forçage} %
\bleu{(A,B) \force 1A \wedge 2B},

\bleu{(A,B) \force K_1(2B \vee 2C},

\bleu{(A,B) \force K_1`! K_2(1A)}.

L'assertion \bleu{K_1(2A \vee 2B \vee 2C)} donc \bleu{\mathcal{M} "|=" K_1(2A \vee 2B \vee 2C)}. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les enfants sales} %
\newcommand{\itemrouge}{\item[\emph{$`.$}]}
  \begin{itemize}
    \itemrouge Il y a \bleu{n} enfants dont certains ont la saleté sur
    le front.  

    \itemrouge Le père déclare «L'un d'entre vous a de la
    saleté sur le front».  

    \itemrouge Puis le père pose plusieurs fois
    (combien ?) la question «Avez-vous de la saleté sur le front ?».
    
    \itemrouge Comme les \bleu{n} enfants ont tous de la saleté sur
    le front.
  
    \itemrouge Après \bleu{n} questions du père, ils répondent tous
    ensemble «oui».
  \end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le modèle de Kripke pour les enfants sales} %
\begin{footnotesize}
\centerline{
\xymatrix @C 20pt @R 20pt {
&  *++[o][F-]{1,1,1} \ar@{-}[ld] \ar@{.}[d]  \ar@{=}[rd]& \\
*++[o][F-]{1,0,1}  \ar@{.}[d]  \ar@{=}[rd] & *++[o][F-]{1,1,0} \ar@{-}[ld] \ar@{=}[rd]& *++[o][F-]{0,1,1} \ar@{-}[ld] \ar@{.}[d]\\
*++[o][F-]{1,0,0} \ar@{=}[rd]& *++[o][F-]{0,0,1} \ar@{.}[d] & *++[o][F-]{0,1,0} \ar@{-}[ld] \\
& *++[o][F-]{0,0,0}
}}
\end{footnotesize}
\vfill
On abandonne les boucles de réflexivité.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Après que le père ait parlé} %
\begin{footnotesize}
\centerline{
\xymatrix @C 20pt @R 20pt {
&  *++[o][F-]{1,1,1} \ar@{-}[ld] \ar@{.}[d]  \ar@{=}[rd]& \\
*++[o][F-]{1,0,1}  \ar@{.}[d]  \ar@{=}[rd] & *++[o][F-]{1,1,0} \ar@{-}[ld] \ar@{=}[rd]& *++[o][F-]{0,1,1} \ar@{-}[ld] \ar@{.}[d]\\
*++[o][F-]{1,0,0} & *++[o][F-]{0,0,1} & *++[o][F-]{0,1,0}  \\
& *++[o][F-]{0,0,0}
}}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Après que le père ait posé sa première question} %
\begin{footnotesize}
\centerline{
\xymatrix @C 20pt @R 20pt {
&  *++[o][F-]{1,1,1} \ar@{-}[ld] \ar@{.}[d]  \ar@{=}[rd]& \\
*++[o][F-]{1,0,1}  & *++[o][F-]{1,1,0} & *++[o][F-]{0,1,1} \\
*++[o][F-]{1,0,0} & *++[o][F-]{0,0,1} & *++[o][F-]{0,1,0}  \\
& *++[o][F-]{0,0,0}
}}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Après que le père ait posé sa deuxième question} %
\begin{footnotesize}
\centerline{
\xymatrix @C 20pt @R 20pt {
&  *++[o][F-]{1,1,1} & \\
*++[o][F-]{1,0,1}  & *++[o][F-]{1,1,0} & *++[o][F-]{0,1,1} \\
*++[o][F-]{1,0,0} & *++[o][F-]{0,0,1} & *++[o][F-]{0,1,0}  \\
& *++[o][F-]{0,0,0}
}}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Correction} %

\VERT{Théorème :} Si \bleu{"|-" `f} alors \bleu{"|=" `f} .
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Pourquoi pas la règle de déduction ?}%

Si on avait la \emph{règle de déduction}

\textit{«De \bleu{G, `f "|-" `j} je déduis \bleu{G "|-"  `f "=>" `j}»}

alors du jugement \bleu{`f "|-" K_i `f} on aurait \bleu{`f "|=" K_i
  `f}, \ali c'est-à-dire \textit{«Si dans tous les mondes de l'univers
  en question, $`f$ est vrai, alors chaque agent $i$ sait $`f$»}

on pourrait déduire \bleu{"|=" `f "=>" K_i `f} \ali c'est-à-dire
\textit{«Si $`f$ est vrai alors chaque agent $i$ sait $`f$»}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Une preuve} %
On peut prouver \bleu{"|-" `f "=>" K_i `! K_i `! `f}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Une preuve} %
On peut prouver \bleu{"|-" `f "=>" K_i `! K_i `! `f}.
\begin{footnotesize}
\begin{displaymathbleu}
  \prooftree
      \prooftree % -
       \justifies "|-" `! K_i `f "=>" K_i `! K_i `! `f
       \using \emph{(\textbf{5})}
      \endprooftree % -
      \qquad
      \prooftree %-
          \prooftree % --
          \justifies "|-" `j
          \using \emph{(Cl)}
          \endprooftree % --
      \qquad  %
          \prooftree %--
          \justifies "|-" K_i `! `f "=>" `!`f %
          \using \emph{(\textbf{T})} 
          \endprooftree  %--
      \justifies "|-" (`! K_i `f "=>" K_i `! K_i `! `f)  "=>" `f "=>" K_i `! K_i `! `f
      \using \emph{(MP)}
     \endprooftree % -
  \justifies "|-" `f "=>" K_i `! K_i `! `f
  \using \emph{(MP)}
  \endprooftree
\end{displaymathbleu}

où \bleu{`j `= (K_i `! `f "=>" `! `f) 
  "=>" (`! K_i `f "=>" K_i `! K_i  `! `f) %
  "=>" `f "=>" K_i `! K_i `! `f} \ali qui est un théorème classique.

Car c'est un instance de \bleu{(B  "=>" `! A)  "=>" (`!B  "=>" C)
  "=>" (A  "=>" C)}.
\end{footnotesize}
\vfill
\end{slide}
%=======================================================
\end{document}
% LocalWords:  émetteur-récepteur the best d'accusé Control Protocol
