diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 35425f0..07e2999 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2675,14 +2675,10 @@ droite \alert{ou à gauche} du symbole « $\vdash$ ». \medskip \itempoint On garde la règle $\inferrule*[left=Ax]{ }{\Gamma,Q \vdash - Q}$, ou on peut en séparer une règle d'qffaibilissement ; et on va -reparler des règles de « contraction » et « coupure » : + Q}$ ; on va reparler des règles de « contraction » et « coupure » : \begin{center} \begin{tabular}{c|c} -$\inferrule*[left=Ax]{ }{Q \vdash Q}$ -&$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$ -\\\hline $\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$ &$\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}$ \end{tabular} @@ -2691,7 +2687,8 @@ $\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$ \end{frame} % \begin{frame} -\frametitle{Calcul des séquents : les règles (intuitionnistes)} +\label{sequent-calculus-connector-rules} +\frametitle{Calcul des séquents : règles (intuitionnistes) des connecteurs} {\footnotesize |