Another presentation of natural deduction proofs.

1 files changed, 49 insertions, 2 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index d7483b1..3746973 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1344,7 +1344,7 @@ Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
 
 \medskip
 
-Introduction et élimination des connecteurs (style « déduction naturelle ») :
+Introduction et élimination des connecteurs en style « déduction naturelle » :
 
 \smallskip
 
@@ -1375,7 +1375,7 @@ $\bot$
 \end{tabular}
 
 {\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont
-  « déchargées ».\par}
+  « déchargées », c'est-à-dire qu'elles disparaissent.\par}
 
 \end{frame}
 %
@@ -1420,4 +1420,51 @@ $\bot$
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Présentation différente}
+
+On peut aussi n'écrire que les conclusions (partie droite du
+signe $\vdash$), à condition d'indiquer pour chaque hypothèse
+déchargée à quel endroit elle l'a été :
+
+\bigskip
+
+{\footnotesize
+\[
+\inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{
+\inferrule*[left=\llap{$\land$Int}]{
+\inferrule*[left=\llap{$\land$Élim$_2$}]{
+\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
+}{B}
+\\
+\inferrule*[right=\rlap{$\land$Élim$_1$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
+}{A}
+}{B\land A}
+}{A\land B \Rightarrow B\land A}
+\]
+\par}
+
+\bigskip
+
+{\footnotesize
+\[
+\inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{
+\inferrule*[left=\llap{$\lor$Élim(\textcolor{mydarkgreen}{$v$},\textcolor{mydarkgreen}{$v'$})}]{
+\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\lor B}
+\\
+\inferrule*[right={$\lor$Int$_2$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v$}}]{ }{A}
+}{B\lor A}
+\\
+\inferrule*[right=\rlap{$\lor$Int$_1$}]{
+\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v'$}}]{ }{B}
+}{B\lor A}
+}{B\lor A}
+}{A\lor B \Rightarrow B\lor A}
+\]
+\par}
+
+\end{frame}
+%
 \end{document}