%% Time-stamp: <modifié par Pierre Lescanne le 16 Oct 2002 à 18h27>
\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{prooftree}
%\usepackage[dvips]{graphicx}
\usepackage[all]{xy}
\usepackage{qsymbols}

%\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{}   

\definecolor{mauve}{rgb}{1,0,1}
\newcommand{\rouge}[1]{{\color{red}#1}}
\renewcommand{\emph}[1]{\rouge{#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}}}
\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

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

\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]{%
{\color{mauve}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\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}\]
\vfill
\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}\]
\vfill
\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}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice 1}

\vspace*{10pt}

\begin{displaymathbleu}
  \prooftree
    \prooftree
      \prooftree
      \neg\neg p, \neg p "|-" \neg\neg p 
      \qquad  %
      \neg\neg p, \neg p "|-" \neg p \
      \justifies  \neg\neg p, \neg p "|-" \bot 
      \using \emph{"=>" E}
      \endprooftree
    \justifies \neg\neg p "|-" p
    \using \emph{RAA}
    \endprooftree
  \justifies "|-" \neg\neg p \Ra p
  \using\emph{"=>" I}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice 2}
\begin{scriptsize}
\begin{displaymathbleu}
  \prooftree % -
  \prooftree % --
  \neg(p \vee \neg p) "|-" \neg(p \vee \neg p) \qquad %
      \prooftree % ---
        \prooftree % ----
            \prooftree % -----
            \neg(p \vee \neg p), p  "|-" \neg(p \vee \neg p) %
            \quad %
                 \prooftree % ++++
                 \neg(p \vee \neg p), p  "|-"  p %
                 \justifies \neg(p \vee \neg p), p  "|-" p \vee \neg p %
                 \using \emph{\vee I}
                 \endprooftree % ++++
            \justifies \neg(p \vee \neg p), p  "|-" \bot % 
            \using \emph{"=>" E}
            \endprooftree % -----
        \justifies \neg(p \vee \neg p) "|-" \neg p %
        \using \emph{"=>" I}
        \endprooftree % ----
      \justifies \neg(p \vee \neg p) "|-" p \vee \neg p %
      \using \emph{\vee I}
      \endprooftree % ---
  \justifies \neg(p \vee \neg p) "|-" \bot %
  \using \emph{"=>" E}
  \endprooftree % --
  \justifies "|-" p \vee \neg p %
  \using \emph{RAA} %
  \endprooftree % -
\end{displaymathbleu}
\end{scriptsize}
 \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}

\vfill
\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} 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  green Prop Intro
