%\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/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 =\color{orange!40}\usefont{OT1}{cmtt}{b}{n},basicstyle=\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\ada{\lstset{numbers=none,language=ada,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}
}


\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 38 \& 39}

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


\caml
\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}


\begin{flushright}
\begin{minipage}[t]{0.5\linewidth}  
\begin{lstlisting}[caption={}]
type atom = int;;

type formule =
  |Faux
  |Atomic of atom
  |Non of formule
  |Et of (formule * formule)
  |Ou of (formule * formule)
  |Implique of (formule * formule)
  |Equiv of (formule * formule);;
\end{lstlisting}
\end{minipage}
\end{flushright}
}
\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}

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

\end{frame}


\begin{frame} \frametitle{connecteurs}
  
\begin{alertblock}{Remarque}
  Il y  a bien  plus de  connecteurs logiques que  ceux évoqués  ici. En
  fait, un connecteur logique est  une fonction totale de $\BR_2^n$ dans
  $\BR_2$. On dit  que $n$ est son \textit{arité}.  Par exemple, $\lnot$
  est un connecteur d'arité 1 et $\land$ est un connecteur d'arité 2.
\end{alertblock}
\end{frame}






\begin{frame} \frametitle{arbres}
 $  s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))$


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

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}
    $  s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))$
  \end{exercice}
\end{frame}


\begin{frame} \frametitle{fonction booléenne}
  \begin{example}
    $$ 
f\colon \begin{array}{rll} \BR_2^3 & \to & \BR_2\\
  (p,q,r) & \mapsto &
 s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))
\end{array}
$$
  \end{example}
\end{frame}


\section{Sémantique}


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


\begin{frame} \frametitle{Valeur sous un environnement}
  
\begin{itemize}
\item $\text{Val}(\bot,v)=0$;
\item si $p$ est une variable atomique alors $\text{Val}(p,v)=v(p)$;
\item    $\text{    Val}(\lnot   p,v)=1$    ssi,
      $\text{ Val}(p,v)=0$ \pause (NÉGATION);
\item    $\text{   Val}(p\land    q,v)=1$  ssi 
      $\text{ Val}(p,v)=\text{ Val}(q,v)=1$ \pause (CONJONCTION);
\item    $\text{    Val}(p\lor   q,v)=0$    ssi,
      $\text{ Val}(p,v)=\text{ Val}(q,v)=0$ \pause (DISJONCTION);
\item  $\text{   Val}(p  \rightarrow   q,v)=0$  ssi,
      $\text{ Val}(p,v)=1$ et $\text{ Val}(q,v)=0$ \pause (IMPLICATION);
\item  $\text{  Val}(p\leftrightarrow   q,v)=1$  ssi,
      $\text{ Val}(p,v)=\text{ Val}(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 $\text{Val}(f,v)$?

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


\pause modèle \pause - satisfiable \pause - tautologie \pause - 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{lstlisting}[caption={}]
val pos : int -> bool = <fun>
\end{lstlisting}

\pause
 \begin{lstlisting}[caption={}]
# pos 3;;
\end{lstlisting}

\pause
 \begin{lstlisting}[caption={}]
- : bool = true
  \end{lstlisting}

\pause


$$
\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{lstlisting}[caption={}]
val pos : int -> bool = <fun>
\end{lstlisting}

\pause
 \begin{lstlisting}[caption={}]
# pos trois;;
\end{lstlisting}

\pause
\begin{lstlisting}[caption={}]
Error:
\end{lstlisting}

\pause

$$
\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: 
