%% Time-stamp: <modifié par Pierre Lescanne le 23 Dec 2001 à 11h32>
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
%\usepackage[all]{xy}

%\renewenvironment{slide}[1]{#1} 
%\def\printlandscape{}  % pour sortir en portrait
%\slidesmag{1} 
%\usepackage{fullpage}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips

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

\slidesmag{5}
\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\rouge{\textit{La logique propositionnelle classique}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\newcommand{\vDash}{\mathbf{\mathtt{\large |\!\!\!=}}}
\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{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\ra}{\ensuremath{\rightarrow}}
\newcommand{\RaE}{\VERT{\Ra E}}
\newcommand{\RaI}{\VERT{\Ra I}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\Arb}{\rouge{{\cal A}}}
 \newcommand{\infer}[2]{\bl{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}}
\newcommand{\inferThreeLabel}[5]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\hspace{2em} #4\\
   \hline \noalign{\vskip 1pt}#5
  \end{array}
\end{array}}}

\newcommand{\inferTwoLabel}[4]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}
\end{array}}}

\newcommand{\leafLabel}[2]{\bl{
 {\VERT{#1}} \quad
  \begin{array}{c}
  #2
  \end{array} }}

\newcommand{\inferLabel}[3]{\bl{
    \begin{array}{cc}
    {\VERT{#1}} \quad
    \begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  \end{array}
  }}

    
\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
  \begin{center}                % mais ca peut t'interesser
    \large\bf
    \color{cyan}{\shadowbox{#1}}%
  \end{center}
  \markright{#1}
  \vspace{1ex minus 1ex}}

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

\begin{document}

%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{En déduction naturelle}
On ajoute la règle dite de \rouge{réduction par l'absurde.}
\[\inferLabel{RAA}{\Gamma, \neg p\vdash\bot}{\Gamma\vdash p}\]
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Attention}: il ne faut pas confondre cela avec
\[\infer{\Gamma, p\vdash\bot}{\Gamma\vdash \neg p}\]
qui est en fait:
\[\infer{\Gamma, p\vdash\bot}{\Gamma\vdash p\Ra \bot}\]
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}
Prouvez
\begin{enumerate}
\item \bleu{\neg\neg p \Ra p}
\item \bleu{p \vee \neg p}
\item \bleu{((p \Ra q) \Ra p) \Ra p}
\end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}

\begin{tiny}
\newcommand{\A}{\neg(p \vee \neg p) \vdash \neg(p \vee \neg p)}
\newcommand{\E}{\inferTwoLabel{\Ra E}{\A}{\Arb}{\neg(p \vee \neg p) \vdash \bot}}

\bl{
\begin{math}
\inferLabel{RAA}{\E}{\vdash p \vee \neg p}
\end{math}
}
\end{tiny}

où

\begin{tiny}
\newcommand{\B}{\inferTwoLabel{\begin{array}{c}\\[2pt]\Ra~E\end{array}}%
  {\neg(p \vee \neg p), p \vdash \neg(p \vee \neg p)}%
  {\AB}{\neg(p \vee \neg p), p \vdash \bot}}
\newcommand{\C}{\inferLabel{\begin{array}{c}\\[10pt]\Ra
      I\end{array}}{\B}{\neg(p \vee \neg p) \vdash \neg p}}
\newcommand{\D}{\inferLabel{\begin{array}{c}\\[20pt]\vee
      I\end{array}}{\C}{\neg(p \vee \neg p) \vdash p \vee \neg p}}
\newcommand{\AB}{\inferLabel{\vee I}{\neg(p \vee \neg p), p \vdash
    p}{\neg(p \vee \neg p), p \vdash p \vee \neg p}} \bl{
\begin{displaymath}
\hspace*{-25pt}
\begin{array}{c}
\\[20pt]
\Arb =
\end{array}
\D
\end{displaymath}
}

\end{tiny}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction et complétude}
\rouge{Interprétation:}  une fonction de \bleu{proposition} vers
\bleu{\{0,1\}}, somme et produit modulo 2.
\begin{itemize}
\item \bleu{v(p \Ra q)} = \bleu{1 + v(p) + v(p).v(q)}
\item \bleu{v(p \vee q)} = \bleu{v(p) + v(q) + v(p).v(q)} 
\item \bleu{v(p \et q)} = \bleu{v(p).v(q)} 
\item \bleu{\bot} = 0
\end{itemize}

\bleu{\Gamma \vDash_{NK} p} signifie que si \bleu{v(q)=1} pour tout
\bleu{q\in\Gamma} alors \bleu{v(p)=1}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction et complétude (suite)}
La logique propositionnelle est \rouge{correcte}, \\ \hspace*{20pt}c-à-d
\bleu{\Gamma\vdash_{NK} p} implique \bleu{\Gamma\vDash_{NK} p} 

\vspace{20pt}

La logique propositionnelle est \rouge{complète}, \\ \hspace*{20pt}c-à-d
\bleu{\Gamma\vDash_{NK} p} implique \bleu{\Gamma\vdash_{NK} p} 
\end{slide}
%------------------------------------------------------
\begin{slide}
\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  green Prop Intro
