%\RequirePackage{atbegshi}
\documentclass[french]{beamer}
\usepackage{etex}

\usepackage[beamer,utf8,fourier]{preambuleTrm}
%\usepackage[french,vlined,boxed]{algorithm2e}
\usepackage{bookmark,multido}
%\usepackage{xlop}



\usepackage{tikz}
\usetikzlibrary{automata,fit,trees,matrix,arrows,decorations.pathmorphing,shapes.arrows,chains,positioning,intersections,backgrounds,calc,through,mindmap}
\newcommand{\myunit}{1.1cm}
\usepackage{tkz-graph,tkz-berge}
\usepackage{circuitikz}


\usepackage{caption}
\captionsetup{labelformat=empty,font=footnotesize}


\usepackage{media9}

%\usepackage{multimedia}
% \usepackage{cclicenses}
% \usepackage{cclicence}
\setbeamertemplate{theorems}[numbered]




\usepackage{algo}

\renewcommand{\algocommentfont}{\small\ttfamily\itshape}

\newcommand\nor{\downarrow}
\newcommand\nand{\uparrow}
\newcommand\xor{\oplus}

\newcommand\foncpart{\rightarrow\!\!\!\!\!\!\shortmid}
\newcommand\fonctot{\rightarrow}
\newcommand\injpart{\rightarrowtail\!\!\!\!\!\!\!\shortmid}
\newcommand\injtot{\rightarrowtail}
\newcommand\surjpart{\twoheadrightarrow\!\!\!\!\!\!\!\shortmid}
\newcommand\surjtot{\twoheadrightarrow}
\newcommand\bijpart{\rightarrowtail\!\!\!\!\!\!\!\shortmid\!\!\!\!\twoheadrightarrow}
\newcommand\bijtot{\rightarrowtail\!\!\!\!\!\!\!\!\!\twoheadrightarrow}


\newtheorem{exercice}{Exercice}


\setlength{\columnseprule}{0pt}

%\setlength{\parskip}{0pt}

\graphicspath{{/home/moi/IUT/PolyINFO1}{/home/moi/Lycee/TDmaple/2006_7/}{/home/moi/Figures/Arbres_Graphes/}{/home/moi/Figures/FigSTI/}{/home/moi/Figures/FigMaple/}{/home/moi/Photos/Maths/}{/home/moi/Photos/Tehessin/}{/home/moi/Figures/FigSTI/}{/home/moi/Figures/FigSeconde/}{/home/moi/Lycee/Informatique/XCAS/2008_9/}{/home/moi/Lycee/TDmaple/2008_9/}{/home/moi/IUT/Thierry/Conversions/}{/home/moi/Photos/informathix/}{/home/moi/Lycee/Informatique/PafAlgo/}}




\newcommand\caml{\lstset{numbers=none,language=Caml,xleftmargin=10pt,%
keywordstyle =\small\color{orange!40}\usefont{OT1}{cmtt}{b}{n},basicstyle=\small\ttfamily\color{white},commentstyle=\normalfont\scriptsize\slshape,breaklines=true,backgroundcolor=\color{black!90!red},frame=trBL,framerule=1pt,framesep=4pt,rulesep=1pt,showstringspaces=false,stringstyle=\slshape,captionpos=b}
}



\newcommand\haskell{\lstset{numbers=none, escapeinside={(*@}{@*)},language=haskell,xleftmargin=10pt,%
keywordstyle =\footnotesize\color{blue!40}\usefont{OT1}{cmtt}{b}{n},basicstyle=\footnotesize\ttfamily\color{white},commentstyle=\normalfont\scriptsize\slshape,breaklines=true,backgroundcolor=\color{black!90!blue},frame=trBL,framerule=1pt,framesep=4pt,rulesep=1pt,showstringspaces=false,stringstyle=\slshape,captionpos=b}
}


\newcommand\prolog{\lstset{numbers=none,language=prolog,xleftmargin=10pt,%
keywordstyle =\color{blue!40}\usefont{OT1}{cmtt}{b}{n},basicstyle=\ttfamily\color{white},commentstyle=\normalfont\scriptsize\slshape,breaklines=true,backgroundcolor=\color{black!90!blue},frame=trBL,framerule=1pt,framesep=4pt,rulesep=1pt,showstringspaces=false,stringstyle=\slshape,captionpos=b}
}




\setcounter{tocdepth}{1} %\setcounter{page}{0}


\renewcommand\FancyVerbFormatLine[1]{\colorbox{green}{#1}}


\mode<presentation>
{
  \usetheme[secheader]{Madrid}
  % or ...Warsaw

  \setbeamercovered{highly dynamic}
  % or whatever (possibly just delete it)
}
\usepackage{elephantbird}



\begin{document}


\title[] % (optional, use only with long paper titles)
{Logique des propositions}

\subtitle{INFO1 - Semaines 36 \& 37}

\author[] % (optional, use only with lots of authors)
{Guillaume CONNAN }
% - Give the names in the same order as the appear in the paper.
% - Use the inst{?} command only if the authors have different
%   affiliation.

\institute{\textsc{IUT} de Nantes - Dpt d'informatique }% (optional, but mostly needed)

\logo{\includegraphics[scale=0.15]{logo_iut}}

%\logo{\includegraphics[scale=0.15]{big_connan}}

\date[] % (optional, should be abbreviation of conference name)
{Dernière mise à jour: \today{} à \now}
% - Either use conference name or its abbreviation.
% - Not really informative to the audience, more for people (including
%   yourself) who are reading the slides online

\subject{ }


\beamerdefaultoverlayspecification{<+->}

% \AtBeginSubsubsection[]
% {
%   \begin{frame}<beamer>
%     \frametitle{Sommaire}
%  {\scriptsize
% \begin{multicols}{2}
%     \tableofcontents[currentsection,currentsubsection]
%        \end{multicols}
% }

%   \end{frame}
% }




% \AtBeginSubsection[]
% {\scriptsize
%   \begin{frame}<beamer>
%     \frametitle{Sommaire}
%  {\tiny
% \begin{multicols}{2}
%     \tableofcontents[currentsection,currentsubsection]
%        \end{multicols}
% }

%   \end{frame}
% }





\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Sommaire}
 {\scriptsize
\begin{multicols}{2}
    \tableofcontents[currentsection]
       \end{multicols}
}

  \end{frame}
}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

\beamerdefaultoverlayspecification{<+->}




\newcommand{\TR}{\mathcal{T}}


\begin{frame}
  \titlepage
\end{frame}

\begin{frame}
 \frametitle{Sommaire}
{\scriptsize
\begin{multicols}{2} 
 \tableofcontents
\end{multicols}
}

 
 \end{frame}





  \begin{frame}
% \includemedia[
% width=0.6\linewidth,height=0.45\linewidth,
% activate=pageopen,
% flashvars={
% modestbranding=1 % no YT logo in control bar
% &autohide=1
% % controlbar autohide
% &showinfo=0
% % no title and other info before start
% &rel=0
% % no related videos after end
% },
% url
% % Flash loaded from URL
% ]{}{http://www.youtube.com/v/Mdc3o7wOwNA?rel=0}
% %
\includemedia[
url,
width=\linewidth,
height=\textheight
]{}{http://youtu.be/lbg6xoS3K3U}

  \end{frame}

  \begin{frame}



\textbf{Dr. McCoy}:\textit{ Mr. Spock, remind me to tell you that I'm sick and tired of your logic.}

\textbf{Spock}: \textit{That is a most illogical attitude.}

\begin{center}
    \href{http://youtu.be/lbg6xoS3K3U}{ \includegraphics[height=0.7\textheight]{spockmccoy}}
  \end{center}
  
  \end{frame}





\section{Test préliminaire}


\begin{frame}
\begin{quote}
{\itshape Soit un  entier naturel $n$ inférieur à 20.  On considère la
  proposition  \og  si   $n$  est  pair,  alors   son  successeur  est
  premier\fg{}. Quels sont les entiers qui rendent cette proposition vraie?}
\end{quote}
\end{frame}





\begin{frame} \frametitle{Réponses}
  
Ça y est? Bon, analysons  les réponses possibles. Notons $E=\llbracket
0,20\rrbracket$. Vous avez répondu...

\begin{itemize}
\item ... \og 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 12, 13, 15, 16, 17, 18, 19\fg{}: vous
  avez triché ou bien vous avez eu un bon cours de logique au lycée et
  vous l'avez bien étudié. La lecture des paragraphes suivants va vous
  permettre d'aller plus loin;
\item ... \og  2, 4, 6, 10,  12, 16, 18\fg{}: c'est  bien, vous n'avez
  pas triché  mais malheureusement ce  n'est pas la bonne  réponse. La
  lecture  des   paragraphes  suivants   devrait  vous   permettre  de
  progresser en logique pour affronter  sereinement vos deux années d'\textsc{Iut}.
\item ...\og tous\fg{}: vous avez eu raison  de ne pas sortir le jeudi soir pour
  travailler et vous remettre à niveau.  La
  lecture  des   paragraphes  suivants   devrait  vous   permettre  de
  découvrir la  logique, l'arithmétique et la  mathématique en général
  pour affronter sereinement vos deux années d'\textsc{Iut}.

\end{itemize}
\end{frame}




\section{Contexte} 


\begin{frame}
  \begin{itemize}
  \item proposition
\item \og \textit{Igor dort}\fg{}
\item prédicats
\item \og \textit{X dort}\fg{}

\item sémantique

\pause Vrai ou Faux?

\item syntaxe

\pause construction des formules

  \end{itemize}
\end{frame}




\haskell



\section{Syntaxe}

\subsection{Les symboles}

\begin{frame}
  \begin{itemize}
\item 
    \textit{propositions   atomiques}. 
\item $\bot$ 

\item $\top$ 
\item $\lnot$ 
\item $\land$ 
\item $\lor$ 
\item $\rightarrow$ 
\item  $\leftrightarrow$ 
\item  \og (\fg{} et \og )\fg{}.

\end{itemize}
\end{frame}



\begin{frame}[fragile]

{\footnotesize
\begin{minipage}[h]{0.45\linewidth}
L'\textit{ensemble des  formules} de la logique  propositionnelle est le
plus petit ensemble $\FR$ tel que:
\begin{itemize}
\item $\bot$ est un élément de $\FR$;\pause
\item toute proposition atomique est un élément de $\FR$;\pause
\item si $p\in \FR$, alors $(\lnot p)\in \FR$;\pause
\item si $p$ et $q$ sont  dans $\FR$, alors $(p\land q)$,\pause $(p\lor q)$,\pause
  $(p \rightarrow q)$,\pause  et $(p \leftrightarrow q)$\pause sont  des éléments de
  $\FR$;\pause
\item il n'y a pas d'autres expressions bien formées que celles décrites
      par les règles précédentes.\pause
\end{itemize}
\end{minipage}

\vspace{-0.65\textheight}
\pause

\begin{flushright}
\begin{minipage}[t]{0.5\linewidth}  
\begin{lstlisting}
type Atome = Char

data Formule =
  Faux
  |Atomic Atome
  |Non Formule
  |Et Formule Formule
  |Ou Formule Formule
  |Imp Formule Formule
  |Equiv Formule Formule 
\end{lstlisting}
\end{minipage}
\end{flushright}
}

\pause

Que remarquez-vous d'un peu bizarre?

\end{frame}



\begin{frame}[fragile]
  \begin{lstlisting}
-- Opérateurs infixes plus pratiques à utiliser
(*@$ \mu $@*) x      = Atomic x
x   (*@\&@*)  y = Et x y
x  (*@ \S @*)  y = Ou x y
x  ==> y = Imp x y
x <==> y = Equiv x y
  \end{lstlisting}

\pause

\begin{lstlisting}
-- exemple de formule
Non (((*@$ \mu $@*) 'p') & ((*@$ \mu $@*) 'q')) <==> (Non ((*@$ \mu $@*) 'p') (*@ \S @*) Non ((*@$ \mu $@*) 'q'))
\end{lstlisting}

\end{frame}



\begin{frame} \frametitle{priorités}
  
\begin{itemize}
\item $\lnot$ est prioritaire sur les autres opérateurs;
\item  $\lor$   et  $\land$  sont  prioritaires   sur  $\rightarrow$  et
  $\leftrightarrow$.
\end{itemize}

\pause

Mais attention! $p\lor q\land r$ est ambigu.

\end{frame}


\begin{frame}[fragile] \frametitle{priorités et Haskell}
  \begin{lstlisting}[caption={}]
infixr 2 & 
x & y = Et x y

infixr 2 (*@ \S @*)
x (*@ \S @*) y = Ou x y
        
infixr 1 ==>
x ==> y = Imp x y

infixr 1 <==>
x <==> y = Equiv x y
  \end{lstlisting}


\pause


\begin{lstlisting}
s ==> (p & (Non (q))) (*@\S@*) (p <==> (Non r))
\end{lstlisting}
\end{frame}


\begin{frame} \frametitle{connecteurs}
  
\begin{alertblock}{Remarques}
   Il y a  bien plus de connecteurs  logiques que ceux évoqués ici:  combien y en
  a-t-il à votre avis?

\pause

 On parle aussi d'\textit{arité} d'un connecteur.  Par exemple, $\lnot$
  est un connecteur d'arité 1 et $\land$ est un connecteur d'arité 2.
\end{alertblock}
\end{frame}






\begin{frame}[fragile] \frametitle{arbres}

\begin{lstlisting}
s ==> (p & (Non (q))) (*@ \S @*) (p <==> (Non r))
\end{lstlisting}


\pause

\begin{center}
\begin{tikzpicture}
[edge from parent fork down,
every node/.style={fill=red!50,rounded corners},
edge from parent/.style={red,thick,draw},level 1/.style={sibling distance=4.5cm},
level 2/.style={sibling distance=2.5cm},
level 3/.style={sibling distance=1.4cm}]
\node{$\rightarrow$}
    child{node[fill=red!50!black]{$s$}}
    child{node{$\lor$}
       child{node{$\land$}
       child{node[fill=red!50!black]{$p$}}
       child{node{$\lnot$}
            child{node[fill=red!50!black]{$q$}}}
       }
       child{node{$\leftrightarrow$}
       child{node[fill=red!50!black]{$p$}}
       child{node{$\lnot$}
            child{node[fill=red!50!black]{$r$}}}
       }
};
\end{tikzpicture}
\end{center}

\end{frame}

\begin{frame} \frametitle{Démonstration par induction}
  
\begin{theorem}
  Si une propriété P portant sur les formules de $\FR$ est telle que:

  \begin{itemize}
  \item toute variable propositionnelle vérifie P;
\item $\bot$ vérifie P;
\item si la formule $p$ vérifie P, alors $(\lnot p)$ vérifie P;
\item  si $p$  et  $q$ vérifient  P,  alors $(p\lor  q)$, $(p\land  q)$,
  $(p\rightarrow q)$ et $(p \leftrightarrow q)$ vérifient P;
  \end{itemize}

\pause

alors toutes les formules de $\FR$ vérifient P.
\end{theorem}

\pause

\begin{exercice}
Toute  formule  de  $\FR$  a  autant de  parenthèses  ouvrantes  que  de
parenthèses fermantes.
\end{exercice}

\end{frame}




\begin{frame} \frametitle{Sous-formules}
  \begin{exercice}

Quelles sont les sous-formules de:

    $  s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))$
  \end{exercice}
\end{frame}


\begin{frame}[fragile] 
  \begin{example}
    $$ 
f\colon \begin{array}{rll} \FR^4 & \to & \FR\\
  (p,q,r,s) & \mapsto &
 s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))
\end{array}
$$
  \end{example}

\pause

\begin{lstlisting}
f_boule :: Formule -> Formule -> Formule -> Formule -> Formule
f_boule p q r s =
  s ==> (p & (Non (q))) (*@\S@*) (p <==> (Non r))
\end{lstlisting}



\end{frame}


\section{Sémantique}


\begin{frame} \frametitle{Valeurs sous un environnement}
  
\begin{definition}
Un \textit{environnement}     (ou \textit{distribution  de   vérité}  ou
\textit{interprétation propositionnelle}) est une application 
des variables atomiques de $\FR$ dans $\BR_2$.
\end{definition}
\end{frame}


\begin{frame} \frametitle{Valeur sous un environnement}
  
\begin{itemize}
\item $\VR(\bot,v)=0$;
\item si $p$ est une variable atomique alors $\VR(p,v)=v(p)$;
\item    $\VR(\lnot   p,v)=1$    ssi,
      $\VR(p,v)=0$ \pause (NÉGATION);
\item    $\VR(p\land    q,v)=1$  ssi 
      $\VR(p,v)=\VR(q,v)=1$ \pause (CONJONCTION);
\item    $\VR(p\lor   q,v)=0$    ssi,
      $\VR(p,v)=\VR(q,v)=0$ \pause (DISJONCTION);
\item  $\VR(p  \rightarrow   q,v)=0$  ssi,
      $\VR(p,v)=1$ et $\VR(q,v)=0$ \pause (IMPLICATION);
\item  $\VR(p\leftrightarrow   q,v)=1$  ssi,
      $\VR(p,v)=\VR(q,v)$ \pause (ÉQUIVALENCE),
\end{itemize}

\pause

  $f=(p\land (q \lor  r))$ et 
 $\langle v(p)=1,\, v(q)=0,\, v(r)=1\rangle$ \pause : \pause $\VR(f,v)$?

\end{frame}



\begin{frame}[fragile]
  \begin{lstlisting}[caption={}]
type Environnement = Dic.Map Atome Bool

-- exemple d'environnement
env1 = Dic.fromList[('p',True),('q',False)]

-- évaluation récursive d'une formule sous un environnement
eval :: Formule -> Environnement -> Bool
eval Faux env        = False
eval (Atomic a) env  = env Dic.! a
eval (Non f) env     = if (eval f env) then False else True
eval (Et f g) env    = if (eval f env) then (eval g env) else False
eval (Ou f g) env    = if (eval f env) then True else (eval g env)
eval (Imp f g) env   = eval (Non (f & (Non g))) env
eval (Equiv f g) env = eval ((f & g) (*@\S@*)  ((Non f) & (Non g))) env 
  \end{lstlisting}
\end{frame}




\begin{frame} \frametitle{Tables de vérité}

$p\lor (\lnot q \rightarrow p)$

\pause

\begin{center}
             \begin{tabularx}{\textwidth}{IZ|ZIZ|Z|ZI}
	     \whline
           \pause    $p$ & \pause   $q$ & \pause   $\lnot q$  & \pause   $\lnot q \rightarrow  p$ & \pause   $p\lor
             (\lnot q \rightarrow p)$\\
             \whline
            \pause   1& \pause  1& \pause  0& \pause  1& \pause  1\\
             \hline
           \pause    1& \pause  0& \pause  1& \pause  1& \pause  1\\
             \hline
           \pause    0& \pause  1& \pause  0& \pause  1& \pause  1\\
             \hline
          \pause     0& \pause  0& \pause  1& \pause  0& \pause  0\\
             \whline
             \end{tabularx}
             \end{center}

\end{frame}


\begin{frame}[fragile]

\begin{lstlisting}
*Main Dic> let p9 = (*@ $ \mu $ @*) 'p' (*@ \S @*) ( Non ((*@ $ \mu $ @*) 'q') ==> (*@ $ \mu $ @*) 'p')
*Main Dic> table_verite p9
[('p',True),('q',True)] --> True
[('p',True),('q',False)] --> True
[('p',False),('q',True)] --> True
[('p',False),('q',False)] --> False
\end{lstlisting}


\end{frame}



\begin{frame}
  Tables de vérité de $\land$, $\lor$, $\limp$, $\lequiv$ ?

\pause

\begin{itemize}
\item $\VR(\bot,v)=0$;
\item si $p$ est une variable atomique alors $\VR(p,v)=v(p)$;
\item    $\VR(\lnot   p,v)=1$    ssi,
      $\VR(p,v)=0$ \pause (NÉGATION);
\item    $\VR(p\land    q,v)=1$  ssi 
      $\VR(p,v)=\VR(q,v)=1$ \pause (CONJONCTION);
\item    $\VR(p\lor   q,v)=0$    ssi,
      $\VR(p,v)=\VR(q,v)=0$ \pause (DISJONCTION);
\item  $\VR(p  \rightarrow   q,v)=0$  ssi,
      $\VR(p,v)=1$ et $\VR(q,v)=0$ \pause (IMPLICATION);
\item  $\VR(p\leftrightarrow   q,v)=1$  ssi,
      $\VR(p,v)=\VR(q,v)$ \pause (ÉQUIVALENCE),
\end{itemize}


\end{frame}




\begin{frame}[fragile]
  \begin{lstlisting}[caption={}]
*Main> table_verite ((*@ $ \mu $ @*) 'p' & (*@ $ \mu $ @*) 'q')
[('p',True),('q',True)] --> True
[('p',True),('q',False)] --> False
[('p',False),('q',True)] --> False
[('p',False),('q',False)] --> False

  \end{lstlisting}
  

\pause


\begin{lstlisting}[caption={}]
*Main> table_verite ((*@ $ \mu $ @*) 'p' (*@\S@*) (*@ $ \mu $ @*) 'q')
[('p',True),('q',True)] --> True
[('p',True),('q',False)] --> True
[('p',False),('q',True)] --> True
[('p',False),('q',False)] --> False
\end{lstlisting}
\end{frame}



\begin{frame}[fragile]


  \begin{lstlisting}[caption={}]
*Main> table_verite ((*@ $ \mu $ @*) 'p' ==> (*@ $ \mu $ @*) 'q')
[('p',True),('q',True)] --> True
[('p',True),('q',False)] --> False
[('p',False),('q',True)] --> True
[('p',False),('q',False)] --> True
  \end{lstlisting}


\pause

\begin{lstlisting}[caption={}]
*Main> table_verite ((*@ $ \mu $ @*) 'p' <==> (*@ $ \mu $ @*) 'q')
[('p',True),('q',True)] --> True
[('p',True),('q',False)] --> False
[('p',False),('q',True)] --> False
[('p',False),('q',False)] --> True
\end{lstlisting}

\end{frame}




\begin{frame}



\begin{definition}
Un \textit{modèle} d'une formule donnée est un environnement pour
lequel la formule est vraie.
\end{definition}

\pause

Par exemple, $\langle v(p)=1, v(q)=0\rangle$ est un modèle de $p\lor (\lnot q \rightarrow p)$.

\end{frame}




\begin{frame}


\begin{definition}
  Une formule est\textit{ satisfiable }si, et seulement si, elle admet au moins un modèle.
\end{definition}
\pause

Par exemple $p\lor (\lnot q \rightarrow p)$ est satisfiable.

\end{frame}




\begin{frame}

\begin{definition}
Une formule $f$ vraie pour toutes les interprétations de ses variables
atomiques est une \textit{tautologie}. On note alors $\models f$.
\end{definition}
\pause
Par exemple, vérifiez que $\models (\lnot p \lor p)$.
\end{frame}




\begin{frame}


\begin{definition}
Une formule qui n'admet aucun modèle est dite \textit{insatisfiable}.
\end{definition}
\pause

Par exemple $\lnot p \land p$ est insatisfiable.


\end{frame}

\subsection{Conséquences et équivalences logiques}

\begin{frame} \frametitle{Conséquence logique}
\begin{definition}
Soit F une formule  ou un ensemble de formules et G  une formule. On dit
que G  est une  \textit{conséquence logique} de  F si, et  seulement si,
tout modèle de F est aussi un modèle de G.
\pause
On note alors $F\models G$.
\end{definition}  
\end{frame}




\begin{frame} \frametitle{Exemple}

\og  Je vous  paierez  seulement  si votre  programme  marche. Or  votre
programme ne marche pas donc je ne vous paierai pas.\fg{}


Notons  $p$ la  variable atomique:  \og Le  client paye\fg{}  et  $m$ la
variable: \og le programme marche\fg{}.


\pause

Si  le client  paye, cela  implique que  le programme  marche donc  on a
$p\rightarrow m$.

\pause

 De plus on sait que $\lnot m$.

\pause

 La conséquence logique
en est $\lnot p$.

\pause

Le raisonnement du client peut donc être modélisé par:

$$p\rightarrow m,\ \lnot m\models \lnot p$$


\pause

Est-il correct? 


\end{frame}





\begin{frame}
  
\og Je vous paierez seulement si  votre programme marche.  Or je ne vous
paierai pas donc votre programme ne marche pas\fg{}

\end{frame}


\begin{frame}
  \begin{alertblock}{Attention!}
     Notez la différence entre $\rightarrow$ et $\models$!...

\pause

$F\models   G$\fg{}  signifie   que  \og  $F\rightarrow   G$  est
  une tautologie\fg{} ou encore \og $\models (F\rightarrow G)$\fg{}.


  \end{alertblock}
\end{frame}

\begin{frame}
  \begin{exercice}
    Remplissez la table suivante:
\begin{center}
             \begin{tabularx}{\linewidth}{Ic|cIc|c|c|c|ZI}
	     \whline
             $p$ &  $m$ & $p\limp m$  & $\lnot m $ & $(p\limp m) \land \lnot m$ & $\lnot p$ & $((p\limp m) \land \lnot m) \limp \lnot p$\\
             \whline
             1&1&&&&&\\
             \hline
             1&0&&&&&\\
             \hline
             0&1&&&&&\\
             \hline
             0&0&&&&&\\
             \whline
             \end{tabularx}
             \end{center}

  \end{exercice}
\end{frame}



\begin{frame} \frametitle{équivalence logique}
  

\begin{definition}
  Soient  F et  G deux  formules. On  dit que  E et  F  sont logiquement
  équivalentes si,  et seulement  si, $F\models G$  et $G\models  F$. On
  note alors $F\equiv G$.
\end{definition}

\end{frame}

\begin{frame}
  
{\footnotesize
\begin{tabularx}{\textwidth}{ll}
\pause Équivalence entre connecteurs & \pause    $p\limp q \equiv \lnot p \lor q$ \\
                            & \pause    $p \lequiv q  \equiv (p \limp q) \land (q
                             \limp  p) \equiv  (p\land  q)\lor (\lnot  p
                             \land \lnot q)$\\
\pause Double négation & \pause    $\lnot\lnot p \equiv p$\\
\pause Lois de \textsc{De Morgan} & \pause    $\lnot (p \land q) \equiv \lnot p \lor \lnot
q\pause  ,\ \ \ \lnot (p \lor q) \equiv \lnot p \land \lnot
                         q$\\
\pause Idempotence & \pause    $p\lor p \equiv p \land p \equiv p $\\

\pause Commutativité & \pause $p\land q \equiv q \land p\pause , \ \ \ p\lor q \equiv q \lor p$\\

\pause Associativité & \pause    $p\land(q\land r)\equiv (p\land q)\land r\equiv p\land
q\land r$\\
& \pause     $p\lor(q\lor r)\equiv (p\lor  q)\lor r\equiv p\lor
q\lor r$\\

\pause Contradiction & \pause    $p\land \lnot p \equiv \bot$\\

\pause Tiers exclus & \pause    $p\lor \lnot p \equiv \top$\\

\pause Lois de domination & \pause $p\lor \top \equiv \top\pause , \ \ \ p\land \bot\equiv\bot$\\

\pause Lois d'identité & \pause $p\lor \bot\equiv p\pause\pause ,\ \ \ p\land \top\equiv p$\\

\pause Distributivité & \pause    $p\lor(q\land r)\equiv (p\lor q)\land (p\lor r)$\\
               & \pause    $p\land(q\lor r)\equiv (p\land q)\lor (p\land r)$\\
\pause Absorption & \pause $p\lor(p\land q)\equiv p\pause , \ \ \ p\land(p\lor q)\equiv p$\\

\end{tabularx}
}
\end{frame}


\subsection{Principe de déduction par réfutation}


\begin{frame} \frametitle{Principe de déduction par réfutation}
  
\begin{theorem}
  Pour montrer que  $P_1,P_2,...,P_n\models C$ il faut et  il suffit que
  la   \textit{formule  de  réfutation}   $P_1\land  P_2\land\cdots\land
  P_n\land (\lnot C)$ soit insatisfiable.
\end{theorem}

\pause

Quelles équivalences de la diapositive précédentes permettent de prouver
ce théorème?

\end{frame}

\subsection{ Système complet de connecteurs}

\begin{frame} \frametitle{Système complet de connecteurs}
  \begin{definition}
On appelle  \textit{système complet de connecteurs}  tout ensemble $\CR$
de connecteurs tel  que toute formule est équivalente  logiquement à une
formule écrite avec les seuls connecteurs de $\CR$. 

Ce système est \textit{minimal} si aucun sous-ensemble strict de $\CR$
 n'est un système complet de connecteurs.
\end{definition}


\pause

Quel SCC non minimal connaissez-vous? 

\pause

Pouvez-vous vous débarrasser d'un connecteur? \pause De deux ? \pause De
trois?...
\end{frame}






\subsection{Formes normales}






\begin{frame} \frametitle{Formes normales}
  

\begin{definition}
  On appelle \textit{littéral} toute formule atomique ou sa négation.
\end{definition}

\pause


\begin{definition}
  Une formule est dite sous \textit{forme normale conjonctive (fnc)} si,
  et seulement  si, elle est composée d'une  conjonction de disjonctions
  de littéraux.

Une formule est dite sous \textit{forme normale disjonctive (fnd)} si,
  et seulement  si, elle est composée d'une  disjonction de conjonctions
  de littéraux.
\end{definition}


\end{frame}




\begin{frame} \frametitle{Formes normales}
  
\begin{theorem}
  Toute formule  de la  LP admet  une fnc minimale  et une  fnd minimale
  uniques,  à  l'ordre  près  des  littéraux, qui  lui  sont  logiquement
  équivalentes.
\end{theorem}
\end{frame}




\begin{frame} \frametitle{Formes normales}
  \begin{exercice}
    \begin{enumerate}
    \item  Écrire  $x\land\neg (\neg  y  \land  z)$  sous forme  normale
          disjonctive.
\item Écrire $\neg(\neg(x  \land y)\land z)\land\neg((\neg x\lor z)\land
      (\neg y\lor\neg z))$
    \end{enumerate}
  \end{exercice}

\pause


\begin{enumerate}
\item on passe au  SCC $\bigl\{\lnot,\land,\lor\bigr\}$ en utilisant les
      équivalences entre connecteurs;
\item  on réduit les  négations pour  n'avoir plus  que des  littéraux à
      l'aide des lois de \textsc{De Morgan} et de la double négation;
\item  distributivité, absorption et  commutativité permettent  enfin de
      conclure selon la forme voulue:
      \begin{itemize}
      \item  $p\lor(q\land r)\equiv  (p\lor q)\land  (p\lor r)$  pour la
            fnc;
\item $p\land(q\lor r)\equiv (p\land q)\lor (p\land r)$ pour la fnd.
      \end{itemize}
\end{enumerate}
\end{frame}

\section{Portes logiques}

\begin{frame} \frametitle{Mode étasunienne}
  \begin{center}
 
\begin{circuitikz} \draw
(0,0) node[and port,color=white] (myand) {}
(5,0) node[or port,color=white] (myor) {}
(9,0) node[not port,color=white] (mynot) {}

(0,-2) node[nand port,color=white] (mynand) {}
(5,-2) node[nor port,color=white] (mynor) {}
(9,-2) node[xor port,color=white] (myxor) {}

(myand.in 1) node[anchor=east] {$x$}

(myand.in 2) node[anchor=east] {$y$}

(myand.out) node[anchor=west] {$x\land y$}

(myor.in 1) node[anchor=east] {$x$}

(myor.in 2) node[anchor=east] {$y$}

(myor.out) node[anchor=west] {$x\lor y$}

(mynot.in) node[anchor=east] {$x$}

(mynot.out) node[anchor=west] {$\lnot x$}


(mynand.in 1) node[anchor=east] {$x$}

(mynand.in 2) node[anchor=east] {$y$}

(mynand.out) node[anchor=west] {$x\nand y$}

(mynor.in 1) node[anchor=east] {$x$}

(mynor.in 2) node[anchor=east] {$y$}

(mynor.out) node[anchor=west] {$x\nor y$}

(myxor.in 1) node[anchor=east] {$x$}

(myxor.in 2) node[anchor=east] {$y$}

(myxor.out) node[anchor=west] {$x\oplus y$}

 ;
\end{circuitikz}
\end{center}


\end{frame}

\begin{frame} \frametitle{Mode européenne}

\begin{center}
 
\begin{circuitikz} \draw
(0,0) node[european and port,color=white] (myand) {}
(5,0) node[european or port,color=white] (myor) {}
(9,0) node[european not port,color=white] (mynot) {}

(0,-2) node[european nand port,color=white] (mynand) {}
(5,-2) node[european nor port,color=white] (mynor) {}
(9,-2) node[european xor port,color=white] (myxor) {}

(myand.in 1) node[anchor=east] {$x$}

(myand.in 2) node[anchor=east] {$y$}

(myand.out) node[anchor=west] {$x\land y$}

(myor.in 1) node[anchor=east] {$x$}

(myor.in 2) node[anchor=east] {$y$}

(myor.out) node[anchor=west] {$x\lor y$}

(mynot.in) node[anchor=east] {$x$}

(mynot.out) node[anchor=west] {$\lnot x$}


(mynand.in 1) node[anchor=east] {$x$}

(mynand.in 2) node[anchor=east] {$y$}

(mynand.out) node[anchor=west] {$x\nand y$}

(mynor.in 1) node[anchor=east] {$x$}

(mynor.in 2) node[anchor=east] {$y$}

(mynor.out) node[anchor=west] {$x\nor y$}

(myxor.in 1) node[anchor=east] {$x$}

(myxor.in 2) node[anchor=east] {$y$}

(myxor.out) node[anchor=west] {$x\oplus y$}

 ;
\end{circuitikz}
\end{center}

\end{frame}


\begin{frame} \frametitle{Circuit logique}
  \begin{exercice}
    Vous  disposez de  deux interrupteurs  commandant une  même ampoule:
    comment modéliser le système de va-et-vient? 
  \end{exercice}
\end{frame}


\begin{frame}
  
%\begin{figure}
\begin{center}
  \includegraphics[width=\textwidth]{vaetvient}
\end{center}
%\end{figure}

\end{frame}


\begin{frame} \frametitle{Circuit logique}
  

\begin{center}
\begin{circuitikz} \draw
(0,4) node[european and port,color=white] (myand1) {}
(3,1) node[european and port,color=white] (myand2) {}
(5,2) node[european or port,color=white] (myor) {}
(0,0) node[european not port,color=white] (mynot1) {}
(0,2) node[european not port,color=white] (mynot2) {}

(myand1.in 1) node[anchor=east] {$x$}

(myand1.in 2) node[anchor=east] {$y$}

(mynot1.in) node[anchor=east] {$y$}

(mynot2.in) node[anchor=east] {$x$}


(mynot1.out) -| (myand2.in 2)

(mynot2.out) -| (myand2.in 1)


(myand1.out) -| (myor.in 1)

(myand2.out) -| (myor.in 2)



%(myor.out) node[anchor=west] {$(x\land y)\lor (\lnot x \land \lnot y)$}

;
\end{circuitikz}
\end{center}




\end{frame}



\section{Approche formelle de la logique propositionnelle}


\subsection{Principe général}

\begin{frame}
  \begin{description}
\item[Axiome]\pause proposition primitive\pause 
\item[Théorème] \pause $\vdash T$\pause 
\item[Règle d'inférence]  \pause prémisses \pause $P_1,P_2,...,P_n\vdash
T$.
\end{description}
\end{frame}


\begin{frame}[fragile]
  



$$
\begin{tabular}{ll}
\pause $(P_1)$ & \pause $I\limp B$\pause \\ 
\pause $(P_2)$ &\pause $I$ \pause \\
\hline 
\pause 
$(T)$ &\pause $B$
\end{tabular}
$$

\pause
\begin{center}
\textit{modus   ponens} 
\end{center}
\end{frame}



\begin{frame}[fragile]


$$
\begin{tabular}{ll}
\pause $(P_1)$ & \pause $I\limp B$\pause \\ 
\pause $(P_2)$ &\pause $\neg B$ \pause \\
\hline 
\pause 
$(T)$ &\pause $\neg I$
\end{tabular}
$$


\pause


\begin{center}
\textit{modus   tollens} 
\end{center}

\end{frame}

\begin{frame}
  \begin{alertblock}{Attention!}
    Notez bien la  différence entre $C\limp N,\ N  \models B$ et $C\limp
    N,\ N \vdash B$!

\pause

approche sémantique / approche syntaxique
  \end{alertblock}
\end{frame}




\begin{frame} \frametitle{Règles d'inférence}
  
\begin{center}
  \begin{tabular}{ll}
    Règle de combinaison & \pause    $A,B\vdash A\land B$\\
\pause
Règle de simplification & \pause    $A\land B\vdash B$\\
\pause
Règle d'addition & \pause    $A\vdash A\lor B$\\
\pause
\textit{Modus ponens} & \pause    $A,A\limp B\vdash B$\\
\pause
\textit{Modus tollens} & \pause   $\lnot B,A\limp B\vdash \lnot A$\\
\pause
Syllogisme hypothétique & \pause    $A\limp B,B\limp C\vdash A\limp C$\\
\pause
Syllogisme disjonctif & \pause    $A\lor B,\lnot B\vdash A$\\
\pause
Règle des cas & \pause    $A\limp B,\lnot A\limp B\vdash B$\\
\pause
Élimination de l'équivalence & \pause    $A\lequiv B\vdash A\limp B$\\
\pause
Introduction de l'équivalence & \pause    $A\limp B,B\limp A\vdash A\lequiv B$\\
\pause
Règle d'inconsistance & \pause    $A,\lnot A\vdash B$
  \end{tabular}
\end{center}

\end{frame}





\subsection{Théorème de la déduction}



\begin{frame} \frametitle{Théorème de la déduction}
  
\begin{theorem}
  Si $A,P\vdash B$, alors $P\vdash A\limp B$.
\end{theorem}

\pause



\begin{enumerate}
\item On fait l'\textit{hypothèse} de A: on le rajoute temporairement aux prémisses;
\item on démontre B en utilisant A et le reste des prémisses;
\item on  fait abstraction de A:  A n'est plus forcément  valide mais on
      obtient la conclusion $A\limp B$.
\end{enumerate}



\end{frame}



\begin{frame} \frametitle{démonstration du syllogisme hypothétique}

\begin{enumerate}
\item $A\limp B$ (première prémisse)
\item $B\limp C$ (deuxième prémisse)
\item  $A$   (on  rajoute  temporairement  A  aux   prémisses:  on  fait
      l'hypothèse de A)
\item $A,A\limp B \vdash B$ d'après le MP en utilisant 3. et 2.: on peut
      mettre B dans les prémisses
\item $B,B\limp C\vdash C$ d'après le MP en utilisant 4. et 2.
\item  on  fait abstraction de A:  A n'est plus forcément  valide mais on
      obtient la conclusion $A\limp C$.
\end{enumerate}

\end{frame}



\begin{frame} \frametitle{Arbre binaire de déduction}


\begin{center}
\begin{tikzpicture}
[edge from parent fork up,grow=north,
every node/.style={fill=red!30!black,rounded corners},
edge from parent/.style={red!70!black,thick,draw},level 1/.style={sibling distance=4.5cm},
level 2/.style={sibling distance=2.5cm},
level 3/.style={sibling distance=1.4cm}]
\node{C}
    child{node[fill=yellow!50!red]{$B\limp C$}}
    child{node{$B$}
       child{node[fill=yellow!50!red]{$A\limp B$}}
       child{node[fill=yellow!50!black]{$A$}}
       };
\end{tikzpicture}
\end{center}

\pause

\begin{center}
\begin{tikzpicture}
[edge from parent fork up,grow=north,
every node/.style={fill=red!30,rounded corners},
edge from parent/.style={red,thick,draw},level 1/.style={sibling distance=4.5cm},
level 2/.style={sibling distance=2.5cm},
level 3/.style={sibling distance=1.4cm}]
\node[fill=yellow!50!black]{$A\limp C$}
    child{node[fill=yellow!50!red]{$B\limp C$}}
    child{node[fill=yellow!50!red]{$A\limp B$}
       };
\end{tikzpicture}
\end{center}
\end{frame}






\subsection{Retour sur la démonstration par réfutation}



\begin{frame}
  
%\begin{figure}
\begin{center}
  \includegraphics[height=\textheight]{invaders}
\end{center}
%\end{figure}

\end{frame}


\begin{frame}\frametitle{Les envahisseurs}
  \og Si John est  un envahisseur, il ne rigolera pas à  mes blagues ou il
aura  le petit  doigt de  la main  droite écarté.  John a  rigolé  à mes
blagues et a le petit doigt  serré contre l'annulaire. Ce n'est donc pas
un envahisseur\fg{}

\pause

Soit E: \og John est un envahisseur\fg{}, \pause R: \og il rigolera de mes
blagues\fg{}, \pause P:\og il a le petit doigt écarté\fg{}.

\pause
Les prémisses sont  donc $E\limp( R \lor P)$,\pause  $\lnot R$,\pause et
$\lnot P$ \pause et
la conclusion $\lnot E$.

\end{frame}









\begin{frame}
  


\begin{center}
\begin{tikzpicture}
[edge from parent fork up,grow=north,
every node/.style={fill=red!30!black,rounded corners},
edge from parent/.style={red,thick,draw},level 1/.style={sibling distance=4.5cm},
level 2/.style={sibling distance=3cm},
level 3/.style={sibling distance=2cm}]
\node{$\bot$}
    child{node[fill=yellow!50!black]{$E$}}
    child{node{$\lnot E$}
       child{node[fill=yellow!50!red]{$\lnot P$}}
       child{node{$\lnot E \lor P$}
            child {node[fill=yellow!50!red]{$\lnot R$}}
            child {node[fill=yellow!50!red]{$\lnot E\lor R\lor P$}}}
       };
\end{tikzpicture}
\end{center}
\end{frame}



\subsection{Clauses de \textsc{Horn} - PROLOG}



\begin{frame}[fragile]\frametitle{Clause de \textsc{Horn}}
  
$$(\lnot P_1\lor \lnot P_2\lor\cdots \lnot P_n)\lor C$$


\pause

$$ (P_1\land
P_2\land ....\land P_n)\limp C$$

\pause

\prolog

\begin{lstlisting}[caption={}]
C :- P1,P2, ... ,Pn.
\end{lstlisting}

\end{frame}


\begin{frame}[fragile]\frametitle{PROLOG}

\prolog

\begin{lstlisting}[caption={}]
parallelogramme :- cote_para,cote_meme_long.
rectangle :- parallelogramme,un_angle_droit.
losange :- parallelogramme,deux_cote_meme_long.
carre :- rectangle,losange.
cote_para.
un_angle_droit.
cote_meme_long.
deux_cote_meme_long.

?- carre.
true.
\end{lstlisting}


\end{frame}

\subsection{Chaînage arrière - PROLOG}

\begin{frame}
  PROLOG: 
on  part du  but à  atteindre et  on recherche  dans notre  catalogue de
connaissances les implications dont notre but est la tête et on continue
jusqu'à arriver à une proposition valide.

\pause

Mais  nous manquons  encore d'outils  mathématiques pour  bien exploiter
PROLOG:  ce sera  l'objet de  notre  module de  novembre sur  \textbf{la
logique des prédicats}...


\end{frame}

\end{document}
%%% Local Variables: 
%%% TeX-master: t
%%% End: