
\setcounter{page}{44}
\setcounter{chapter}{2}
\chapterimage{spock}
\chaptertext{La logique  est omniprésente  en informatique, dès  le plus
bas niveau de l'architecture des ordinateurs (tout dépend en effet de petites
portes  logiques qui laissent  ou ne  laissent pas  passer le  courant) mais
aussi dans le domaine de pointe de l'intelligence artificielle où un \og
robot\fg{} est  confronté au problème  de conséquence logique:  à partir
d'un certain nombre de connaissances acquises, que puis-je en déduire?
Il existe de plus des  langages utilisant une programmation dite logique
comme le célèbre PROLOG.

Nous ne ferons dans un  premier temps qu'étudier sommairement la logique
des propositions,  c'est-à-dire une logique  en dehors de  tout contexte
(spatial, temporel,...)
}



\setlength{\topsep}{1pt}
\setlength{\parskip}{1pt}
\setlength{\partopsep}{1pt}
\setlength{\parsep}{1pt}
\chapter{Logique des propositions}


\begin{flushright}
  \begin{quote}
    {\itshape
% \textbf{Kirk}: I suppose you're about to remind me that logic alone dictates your actions?

% \textbf{Spock}: I would not remind you of that which you know so well. 


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

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

}

  \end{quote}

in \og Star Trek: The Galileo Seven \fg{} (1967)
\end{flushright}



\section{Contexte :-)} 

On appellera \textit{proposition} tout  énoncé dont on peut décider s'il
est vrai ou faux indépendamment de ses composantes.

On  distinguera   la  logique  des   propositions  de  la   logique  des
\textit{prédicats} qui  introduit des variables dans  les assertions qui
peut  les rendre  donc parfois  vraies et  parfois fausses.


Par exemple \og \textit{Igor dort}\fg{} est une proposition susceptible d'être
vraie ou  fausse dans toute situation  alors que la valeur  de vérité de
\og \textit{x dort}\fg{} dépend de $x$.

Nous  distinguerons  également la  \textit{syntaxe}  de  la logique  des
propositions de sa \textsc{sémantique}.

Le dictionnaire propose les définitions suivantes: 

\begin{itemize}
\item \textbf{syntaxe}:
n.  f. (bas  latin  syntaxis, du  grec  suntaksis, ordre)  Partie de  la
grammaire qui décrit les  règles par lesquelles les unités linguistiques
se combinent en phrases. 

\item \textbf{sémantique}:
n. f. (bas latin semanticus, du grec sêmantikos, qui signifie)
\textbf{1.} Étude du sens des unités linguistiques et de leurs combinaisons.
\textbf{2.} Étude  des propositions d'une théorie déductive  du point de
vue de leur vérité ou de leur fausseté. 

\end{itemize}
  

L'étude  de  l'aspect  syntaxique   consiste  à  préciser  comment  l'on
construit les formules et l'aspect sémantique interprète les formules en
terme de \textit{Vrai} ou \textit{Faux}.

\section{Syntaxe}

\subsection{Les symboles}

On\footnote{Le programmeur  ou la  machine...} doit d'abord  vérifier si
les  formules  sont  bien  écrites.   On  a  donc  d'abord  besoin  d'un
alphabet\footnote{Notion  qui  sera   développée  lors  de  l'étude  des
langages et automates}, c'est-à-dire un ensemble de symboles.

L'alphabet du langage de la logique des propositions est constitué de:

\begin{itemize}
\item  un  ensemble  fini  ou infini  dénombrable  de  \textit{variables
    propositionnelles}.   Ce    sont   les   atomes    ou   plutôt   les
    \textit{propositions   atomiques}.  Il   s'agit  des   plus  petites
    propositions pouvant être soit vraies,
    soit fausses. Par exemple: \og Le prof de maths est génial\fg{}.
\item la \textit{constante} logique $\bot$  qui se lit \og FAUX\fg{}. On
      peut parfois également introduite la variable $\top$ qui se lit \og VRAI\fg{}.
\item les \textit{connecteurs} $\lnot$ (NON), $\land$ (ET), $\lor$ (OU),
  $\rightarrow$ (IMPLIQUE) et $\leftrightarrow$ (ÉQUIVALENT);
\item les parenthèses \og (\fg{} et \og )\fg{}.

\end{itemize}
 

Le connecteur  $\lnot$ est un  \textit{connecteur unaire} et  les autres
sont des \textit{ connecteurs binaires}.

L'\textit{ensemble des  formules} de la logique  propositionnelle est le
plus petit ensemble $\FR$ tel que:

\begin{itemize}
\item toute variable propositionnelle est un élément de $\FR$;
\item $\bot$ est un élément de $\FR$;
\item si $p\in \FR$, alors $(\lnot p)\in \FR$;
\item si $p$ et $q$ sont  dans $\FR$, alors $(p\land q)$, $(p\lor q)$,
  $(p \rightarrow q)$,  et $(p \leftrightarrow q)$ sont  des éléments de
  $\FR$;
\item il n'y a pas d'autres expressions bien formées que celles décrites
      par les règles précédentes.
\end{itemize}

\begin{remarque}
Vous  aurez  remarqué  que  l'ensemble  $\FR$ est  défini  à  partir  de
lui-même: ça vous dit quelque chose? 
\end{remarque}


Par exemple, $s\rightarrow ((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))$ est une
proposition mais $\lnot \land(p)\lor$ ne l'est pas.

On  peut se passer  de quelques  parenthèses en  adoptant les  règles de
priorité suivantes:

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


\begin{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{remarque}

\subsection{Représentation à l'aide d'arbres}

Une   formule    logique   peut   être   représentée    par   un   arbre
binaire.  Reprenons  la formule  introduite  plus  haut: $  s\rightarrow
((p\land (\lnot q))\lor(p\leftrightarrow (\lnot r)))$

\begin{center}
\begin{tikzpicture}
[edge from parent fork down,
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{$\rightarrow$}
    child{node[fill=yellow]{$s$}}
    child{node{$\lor$}
       child{node{$\land$}
       child{node[fill=yellow]{$p$}}
       child{node{$\lnot$}
            child{node[fill=yellow]{$q$}}}
       }
       child{node{$\leftrightarrow$}
       child{node[fill=yellow]{$p$}}
       child{node{$\lnot$}
            child{node[fill=yellow]{$r$}}}
       }
};
\end{tikzpicture}
\end{center}




Si   une  formule   contient  au   moins  un   connecteur,   on  appelle
\textit{connecteur principal} de la  formule le connecteur qui se trouve
à la racine de l'arbre (ici c'est $\rightarrow$).



\subsection{Démonstration par induction}


\begin{theoreme}
  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{theoreme}


Ce théorème permet par exemple de prouver le théorème suivant:

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

La preuve est laissée en exercice.

\subsection{Sous-formules}

Nous n'entrerons pas dans les détails mais on peut définir par induction
les sous-formules d'une formule  donnée: on retiendra juste qu'il s'agit
de toutes les formules apparaissant dans une formule donnée.

Par exemple, l'ensemble des sous-formules de $(p\rightarrow q)\lor
\lnot(q\leftrightarrow r)$ est $$\bigl\{p\rightarrow q,
\lnot(q\leftrightarrow r),q\leftrightarrow r,p,q,r\bigr\}$$

\subsection{Fonction booléenne}


On considère  un ensemble $\BR_2=\bigl\{0,1\bigr\}$  ou $\bigl\{F,V\bigr\}$ ou
$\bigl\{{\rm Oui},{\rm Non}\bigr\}$, etc.




Une  fonction  booléenne  à  $n$  arguments est  une  fonction  de  type
$\BR_2^n\rightarrow \BR_2$.


Par exemple:

$$
 f\colon \begin{array}{rll} \BR_2^3 & \to & \BR_2\\
  (p,q,r) & \mapsto & (p\rightarrow q)\lor
\lnot(q\leftrightarrow r)
 \end{array}
$$



\section{Sémantique}


Si l'on dispose d'une formule  bien formée, on va pouvoir s'intéresser à
sa valeur de vérité selon les \og mondes\fg{} possibles, c'est-à-dire en
remplaçant chacune des propositions  atomiques qui la composent par VRAI
ou FAUX. On a alors  effectué une \textit{interprétation} de la formule:
c'est une fonction de l'ensemble des formules dans $\BR_2$.

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

La valeur  de vérité d'une  formule va dépendre de  l'environnement dans
lequel on décide d'évaluer la formule.


La \textit{valeur booléenne} d'une  formule $f$ \textit{sous l'environnement} $v$
est définie récursivement par:

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

avec $p$ et $q$ des éléments quelconques de $\FR$.
%\end{definition}

\begin{recherche}
Soit  la formule $f=(p\land (q \lor  r))$ et l'environnement
 $\langle v(p)=1,\, v(q)=0,\, v(r)=1\rangle$. Déterminez $\text{Val}(f,v)$.
\end{recherche}



\begin{NB}
  Notez bien la différence entre $\bot$ et 0! $\bot$ est une proposition
  appartenant à  l'alphabet de la  logique des propositions alors  que 0
  est   la  valeur   prise   par  cette   proposition   sous  tous   les
  environnements: c'est un élément de $\BR_2$.

Par exemple, $\text{Val}(\bot,\langle 0,1,1\rangle) = 0 $.
\end{NB}

\subsection{Tables de vérité}

Lorsqu'une formule ne fait intervenir que peu de variables atomiques, on
peut regrouper dans un tableau  (une \textit{table de vérité}) les $2^n$
(pourquoi?) distributions de vérité possibles.


Considérons par exemple la formule $p\lor (\lnot q \rightarrow p)$:

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


\subsection{Tautologies, formules satisfiables, insatisfiables}


Un peu de vocabulaire....

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


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



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


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


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

Par exemple, vérifiez que $\models (\lnot p \lor p)$.


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


Par exemple $\lnot p \land p$.


\subsection{Conséquences et équivalences logiques}

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

On note alors $F\models G$.
\end{definition}




\begin{recherche}
Prenons un exemple concret. Votre maître de stage vous dit:


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


Ce raisonnement est-il correct?

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

Si  le client  paye, cela  implique que  le programme  marche donc  on a
$p\rightarrow m$. De  plus on sait que $\lnot  m$. La conséquence logique
en est $\lnot p$.

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

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

Est-il correct? 


Et celui-ci:

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

\end{recherche}



\begin{NB}
  Notez la différence entre $\rightarrow$ et $\models$!... En fait
  \og  $F\models   G$\fg{}  signifie   que  \og  $F\rightarrow   G$  est
  une tautologie\fg{} ou encore \og $\models (F\rightarrow G)$\fg{}.

Si F est un ensemble de formules, \og $F_1,F_2,...F_p \models G$\fg{} signifie \og$(F_1\land F_2\land\cdots\land F_p)\rightarrow G$ est une tautologie\fg{}.
\end{NB}


\begin{recherche}
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}


Des remarques?

\end{recherche}



\subsection{Formules d'équivalence de la logique des propositions}




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



Prouvez les différentes équivalences  logiques suivantes qui nous seront
fort utiles:


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

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

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

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

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

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

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

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

\end{tabular}




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



Voici un principe  très utilisé qui utilise des  équivalences du tableau
précédent: trouvez lesquelles...


\begin{theoreme}
  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{theoreme}

On dit alors qu'on a montré la validité par réfutation de la conclusion.

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


On montre le plus souvent qu'un ensemble est un S.C.C. par induction.

Par exemple, nous montrerons en exercice que $\bigl\{\lnot,\land\bigr\}$
et même $\nand$ sont des S.C.C.


\subsection{Formes normales}


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

Par exemple $p$, $\lnot r$.

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



\begin{theoreme}
  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{theoreme}

Afin  d'obtenir ces  formes  normales, qui  seront  importantes pour  un
traitement automatique par une machine, on suit l'algorithme suivant:


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

\section{Portes logiques}

L'informatique,   concrètement,    c'est   au   départ    des   circuits
électroniques: ça passe ou ça ne passe pas. Les calculs dans une algèbre
de Boole sont  donc tout à fait adaptés. On trouve  dans le commerce des
composants  électroniques  modélisant  les  fonctions NOT,  OR,  AND  et
également NOR, NAND, XOR que nous avons étudiées en exercice.

Voici leur représentation à la mode américaine:
\begin{center}
 
\begin{circuitikz} \draw
(0,0) node[and port] (myand) {}
(5,0) node[or port] (myor) {}
(9,0) node[not port] (mynot) {}

(0,-2) node[nand port] (mynand) {}
(5,-2) node[nor port] (mynor) {}
(10,-2) node[xor port] (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=\lnot(x \land y)$}

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

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

(mynor.out) node[anchor=west] {$x\nor y=\lnot(x\lor 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}



et à la mode européenne:


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

(0,-2) node[european nand port] (mynand) {}
(5,-2) node[european nor port] (mynor) {}
(9,-2) node[european xor port] (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}

L'Europe,  c'est   mieux,  alors  on   adoptera  la  deuxième   série  de
représentations.

Construisons  par  exemple  un   circuit  correspondant  à
$f(x,y)=(x\land y)\lor (\lnot x \land \lnot y)$:



\begin{center}
\begin{circuitikz} \draw
(0,4) node[european and port] (myand1) {}
(3,1) node[european and port] (myand2) {}
(5,2) node[european or port] (myor) {}
(0,0) node[european not port] (mynot1) {}
(0,2) node[european not port] (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}




Construisez  les circuits  correspondant  à $(x\land  y\land z)\lor  (x
\land \lnot
y\land z)$ et
$x\land z$. Des remarques?



Pouvoir placer  un maximum  de circuit  sur un même  chip est  une tâche
importante. Pour  cela, il faut que  les circuits soient  les plus petits
possibles tout en effectuant les tâches requises. 

C'est un problème qui peut  devenir compliqué et même actuellement, on a
du  mal à  mettre  au  point des  algorithmes  traitant des  expressions
booléennes dépassant 25 littéraux.

\begin{recherche}
Si vous héritez  d'un semi-remorque de circuits NAND, vous
allez pouvoir construire des ordinateurs: pourquoi?
\end{recherche}
\section{Approche formelle de la logique propositionnelle}

\subsection{Principe général}

Vous avez  créé sur  \textsc{Caml} une fonction  de type  \texttt{int ->
bool}. Vous  l'appliquez ensuite à 3,  qui est de  type \texttt{int}: le
résultat sera  forcément de type  \texttt{bool}: il s'agit  d'un exemple
d'application de  la règle du \textit{Modus Ponens},  très importante en
informatique. C'est la machine qui a trouvé ça toute seule, on regardant
juste la \textit{syntaxe} et  non pas en étudiant la \textit{sémantique}
comme aurait tendance à le faire un humain.




Pour pouvoir  effectuer une déduction logique uniquement  à l'aide d'une
analyse syntaxique, on utilise trois outils:

\begin{description}
\item[Axiome]  : c'est  une proposition  primitive, admise  a  priori et
considérée   comme   non   démontrable   (Par  exemple,   en   géométrie
euclidienne, celle  du collège  et du lycée,  on considère que  par deux
points  distincts il ne  passe qu'une  seule droite.  On ne  le démontre
pas, on  le pose  comme axiome. Dans  d'autres géométries,  on n'utilise
pas cet  axiome et plusieurs droites  peuvent passer par  un même couple
de points...).
\item[Théorème]: c'est  une proposition obtenue à partir  des axiomes ou
d'autres théorèmes à l'aide de règles
appliquées aux symboles  la constituant (ce sont des  règles portant sur
la syntaxe). 

Si T est un théorème, on note $\vdash T$.
\item[Règle d'inférence]  schéma de raisonnement  permettant de produire
de nouveaux théorèmes  à partir de \textit{prémisses} qui  sont soit des
théorèmes, soit des hypothèses.

Si $P_1,P_2,...,P_n$ sont les prémisses et $T$ le théorème, on note
 $P_1,P_2,...,P_n\vdash T$.
\end{description}

Voyons tout de suite un exemple:


\og Si je travaille en cours, j'aurai une bonne note. Or je travaille en
cours 
donc j'aurai une bonne note.\fg{}

Ce raisonnement  est-il correct?  Représentons le schéma  de raisonnement
sous une forme canonique.

Notons $C$: \og Je travaille en cours\fg{} et $N$: \og j'ai une bonne note\fg{}.

$$
\begin{tabular}{ll}
  $(P_1)$ & $C\limp N$\\
  $(P_2)$ & $C$\\
\hline
$(T)$ & $N$
\end{tabular}
$$

Cette règle  d'inférence est  très importante et  porte le nom  latin de
\textit{modus   ponens}  (en  latin,   \textit{ponere}  veut   dire  \og
poser\fg{}. Cela veut donc dire \og posant C on a N\fg{} ;-).

On peut donc écrire: $$C\limp N,\ N \vdash B$$

\begin{remarque}
  Notez  bien  la  différence  avec  $C\limp  N,\  N  \models  B$!  Pour
  l'obtenir,  on  utilise  des  tables  de vérité,  on  étudie  donc  la
  sémantique des propositions.  Dans le cas de $C\limp  N,\ N \vdash B$,
  on  \textit{regarde} juste  si le  schéma  correspond à  l'une de  nos
  règles, en l'occurrence ici le \textit{modus ponens}.  Cette dernière façon de
  prouver convient bien à une machine.


Quand  l'approche  formelle  rejoint  l'approche sémantique,  on  a  un
système     logique    qui     est     dit    \textit{consistant}     et
\textit{complet}. C'est  le cas  de la LP  mais ce  n'est pas le  cas de
toutes les logiques, mais ceci est une autre histoire...

Ainsi, dans le cadre de notre cours, on
a $A \models B$ si, et seulement si, $A\vdash B$.
\end{remarque}


Voyons maintenant un autre exemple:

\og  Si je  travaille en  cours,  j'aurai une  bonne note.  Or j'ai  une
mauvaise note donc je ne travaille pas en cours\fg{}.

Avec les notations précédentes, on obtient:

$$
\begin{tabular}{ll}
  $(P_1)$ & $C\limp N$\\
  $(P_2)$ & $\lnot N$\\
\hline
$(T)$ & $\lnot C$
\end{tabular}
$$


Ce  schéma est correct  et s'appelle  \textit{modus tollens}  (en latin,
\textit{tollere} signifie enlever).


Voici un petit tableau des principales règles dans le système de
\textsc{Hilbert} où A, B et C sont des
formules quelconques:

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

\begin{idee}
La dernière  règle est  rigolote: avec des  prémisses absurdes,  on peut
démontrer n'importe quoi...
\end{idee}


\begin{remarque}
Il existe  d'autres systèmes formels de  la LP, notamment  le système de
\textsc{Lukasiewicz} qui n'a que trois axiomes:

\begin{enumerate}
\item $A\limp(B\limp A)$
\item $(A\limp (B\limp C))\limp ((A\limp B)\limp(B\limp C))$
\item $(\lnot A\limp\lnot B)\limp(B\limp A)$
\end{enumerate}

avec comme unique règle d'inférence le \textit{modus ponens}.


\end{remarque}

\begin{recherche}
Considérons par exemple  le petit jeu suivant: vous  êtes Frodon et vous
vous rendez à Mordor. Vous
arrivez à un embranchement. Deux  envoyés de Saroumane vous donnent chacun
un renseignement. Le premier dit \og Une au moins des deux routes mène à
Mordor\fg{}. Le deuxième dit \og La route de droite ne mène pas à Mordor
mais au repaire de Balrog\fg{}. Saroumane croit se jouer de vous en vous
précisant  que soit  les deux  créatures  disent la  vérité, soit  elles
mentent toutes les deux. Il ne sait pas que vous avez suivi des cours de
logique...Quel route allez-vous prendre?
\end{recherche}

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

L'utilisation  de ces règles  est grandement  facilitée par  le théorème
suivant que nous  admettrons: si on a une  démonstration d'une formule B
utilisant une hypothèse A alors  on peut construire une démonstration de
$A\limp B$ qui n'utilise plus cette hypothèse...en d'autres termes:

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


L'algorithme est le suivant:

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

Démontrons   par  exemple  le   syllogisme  hypothétique   en  utilisant
uniquement le \textit{modus ponens} (MP).


Les prémisses au départ sont $A\limp B$ et $B\limp C$:

\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 1.: 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}

L'emploi d'un \textit{arbre} binaire \textit{de déduction} est peut-être plus claire. Les n\oe uds sont
 des  prémisses   ou  des  arbres   de  déduction.  La  racine   est  la
 conclusion.  Le  théorème de  déduction  consiste  donc  à rajouter  la
 feuille A puis à la couper et remplacer la racine B par $A\limp B$:



\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{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]{$A$}}
       };
\end{tikzpicture}
\end{center}

donne le nouveau théorème:

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


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



On  peut s'inspirer  de  cette  méthode pour  retrouver  le principe  de
démonstration par réfutation. Prenons par exemple le raisonnement suivant
émis par David \textsc{Vincent}:
\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{}

Ajoutons dans les prémisses la  réfutation de la conclusion et voyons ce
qui se passe...

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

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

Rappelons le principe de la réfutation:  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.

Nous allons donc mettre nos prémisses sous forme normale conjonctive.

Or $A\limp  B \equiv \lnot  A \lor B$  donc $E\limp( R  \lor 
P)\equiv \lnot E\lor(R\lor P)\equiv\lnot E\lor  R\lor P $. Tout est donc
prêt...Rajoutons la négation de la conclusion à nos prémisses, à savoir E.







\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{$\bot$}
    child{node[fill=yellow]{$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}

La  conclusion étant  $\bot$, notre  hypothèse  $E$ est  donc fausse  et
heureusement pour David \textsc{Vincent}, John n'est pas un envahisseur.

\begin{idee}
Un raisonnement effectué à l'aide d'un arbre: c'est magique non? En tout
cas, ça  rend la chose programmable,  ce qui ne saurait  manquer de vous
interpeller....

\end{idee}

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

Une  clause de  littéraux n'ayant  qu'un seul  littéral positif  est une
clause    de   \textsc{Horn}\footnote{Alfred    \textsc{Horn},   (1918-2001),
mathématicien  américain.}: c'est  un cas  particulier de  fnc qui  a un
intérêt  certain du fait  de l'équivalence:  $$\lnot A  \lor B  \equiv A
\limp B$$

En effet, une clause de \textsc{Horn} s'écrit:

$$(\lnot P_1\lor \lnot P_2\lor\cdots \lnot P_n)\lor C$$

formule équivalente à:

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


Le   langage  PROLOG   est  basé   sur  l'utilisation   de   clauses  de
\textsc{Horn}.  Par exemple, la règle $ (P_1\land
P_2\land ....\land P_n)\limp C$ s'écrit:

\prolog

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

Un fait  est juste  le fait suivi  d'un point:  \lstinline+P1,P2.+.  Une
question sur un but: \lstinline+?- C.+.

Par exemple:


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

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


Le principe utilisé jusqu'ici, le chaînage avant,  correspondant au théorème de la
déduction, est  le suivant: tous  les prémisses d'une  implication étant
connues, on ajoute  la conclusion à la base  des connaissances, selon le
principe du \textit{modus ponens}.  On
continue jusqu'à ce que:
\begin{itemize}
\item on ne puisse plus rien déduire;
\item on obtient le résultat recherché.
\end{itemize}

On dit que le raisonnement  est \textit{guidé par les connaissances déjà
acquises}.


Il existe une autre manière de procéder, le chaînage arrière, qui constitue le principe du
moteur d'inférence du langage 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.



%











%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\modeexercice % entre en mode exercice
\section{EXERCICES}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\small
%\begin{listeexercices}


\begin{exercice}
On  considère les  propositions atomiques  B, T,  V, C  représentant les
assertions  suivantes:  \og  Hélène   est  belle\fg{},  \og  Hélène  aime
le thé vert\fg{}, \og Hélène porte une robe violette\fg{}, \og Chri-Chri
aime   Hélène\fg{}.   Énoncez  des   phrases   simples  traduisant   les
propositions suivantes:
\begin{enumerate}
\item 
\begin{multicols}{3}
  \begin{enumerate}
  \item $\lnot B$
\item $\lnot B \land \lnot T$
\item $\lnot(B\lor T)$
\item $(B\land V)\limp C$
\item $C\limp(B\lequiv V)$
\item $((B\lor T)\land \lnot V)\limp \lnot C$
  \end{enumerate}
  \end{multicols}
\item 

Traduisez par une proposition simple les phrases 
\begin{enumerate}
\item \og Chri-Chri aime Hélène
seulement si elle porte une robe violette\fg{}.
\item  \og Chri-Chri aime Hélène
 si elle porte une robe violette\fg{}.
\item   \og Chri-Chri aime Hélène
si, et seulement si, elle porte une robe violette\fg{}.
\item \og Si Chri-Chri aime Hélène
alors elle porte une robe violette\fg{}.
\item \og Si Hélène porte une robe violette alors Chri-Chri l'aime\fg{}.
\item \og  Il est suffisant qu'Hélène  porte une robe  viloette pour que
      Chri-Chri l'aime\fg{}.
\item \og  Il est nécessaire qu'Hélène  porte une robe  viloette pour que
      Chri-Chri l'aime\fg{}.
\end{enumerate}

\end{enumerate}
\end{exercice}


\begin{exercice}
Commentez  les   phrases  suivantes  en  fonction  de   la  logique  des
propositions:
\begin{multicols}{2}
\begin{enumerate}
\item Si la Terre est ronde alors $2+2=5$;
\item Si $2+2=5$ alors la Terre est ronde;
\item Si $2+2=5$ alors la Terre est plate.
\end{enumerate}
\end{multicols}
\end{exercice}



\begin{exercice}
On considère les deux propositions:
\begin{itemize}
\item A:\og Si je porte une robe violette alors Chri-Chri m'aime\fg{};
\item B: \og Si Chri-Chri m'aime alors je ne porte pas de robe violette\fg{}.
\end{itemize}
La proposition $A\land B$ est-elle satisfiable?

\end{exercice}



\begin{exercice}
  Prouvez,  à  l'aide de  tables  de  vérité,  la distributivité  de  la
  disjonction sur la conjonction, la première loi de \textsc{De Morgan},
  la règle d'absorption.
\end{exercice}


\begin{exercice}
  Déterminez une table de vérité du connecteur IFTE défini sur $\BR_2^3$
  par $IFTE(x,y,z)=1$ si,  et seulement si, \texttt{if x  then y else z}
  est valide.
\end{exercice}


\begin{exercice}
  L'implication est-elle associative?
\end{exercice}

\begin{exercice}
 Que signifie: \og Il ne m'arrive jamais de n'avoir à me plaindre de rien.\fg{}
\end{exercice}


\begin{exercice}
Montrez que  le produit  d'un irrationnel par  un rationnel non  nul est
toujours  un  irrationnel.  Avez-vous  raisonné  par  l'absurde  ou  par
contraposée? 
\end{exercice}


\begin{exercice}
%On définit deux  opérateurs:
\begin{itemize}
\item L'opérateur $\nor$ est défini par $1\nor 1=1\nor 0=0\nor 1=0$ et
  $0\nor0=1$ qu'on appellera \og NOR\fg{};
\item L'opérateur $\nand$ est défini par $1\nand 0=0\nand
  1=0\nand 0=1$ et $1\nand 1=0$ qu'on appellera \og NAND\fg{}.
\end{itemize}
Montrer que:
\begin{multicols}{3}
  \begin{enumerate}
  \item $ \lnot x\equiv x\nand x\equiv x\nor x$ \item $ x\land y\equiv (x\nand y)\nand(x\nand
    y)$
  \item $ x\lor y\equiv (x\nand x)\nand(y\nand y)$
\item $x\land y\equiv (x\nor x)\nor(y \nor y)$
\item $x\lor y\equiv (x\nor y)\nor(x\nor y)$
  \end{enumerate}
\end{multicols}
\end{exercice}





\begin{exercice}
   Le connecteur$\oplus$ est défini par:
 $1\oplus 1=0$, $ 1\oplus 0=1$, $ 0\oplus 1=1$ et $ 0\oplus 0=0$.
\begin{enumerate}
\item Simplifier:
  \begin{enumerate}
   \begin{multicols}{4}
  \item $x \oplus 0$ \item $x\oplus 1$
  \item $ x\oplus x$ \item $ x \oplus \lnot x$
  \end{multicols} 
\end{enumerate}

\item Montrer que:
\begin{multicols}{2}

  \begin{enumerate}
  \item $x \oplus y\equiv \left(x\lor y\right)\land \lnot\left(x\land y\right)$
  \item $ x\oplus y\equiv \left(x\land \lnot y\right)\lor\left(\lnot x \land y\right)$
  \end{enumerate}
\end{multicols}

\item L'opération $\oplus$ est-elle commutative?

\item Vrai ou faux?
\begin{multicols}{3}

  \begin{enumerate}
  \item $  x \oplus \left(y\oplus  z\right)\equiv \left(x\oplus y\right)\oplus
    z$
  \item $x\lor\left(y\oplus z\right)\equiv (x\lor y)\oplus(x\lor z)$
\item $x \oplus(y\lor z)\equiv (x\oplus y)\lor (x\oplus z)$
  \end{enumerate}
\end{multicols}
\end{enumerate}
\end{exercice}




\begin{exercice}
On consid\'{e}re la fonction bool\'{e}enne de 4 variables d\'{e}finie par : 

$$f=(a\land  \lnot b\land  c)\lor  (\lnot a\land  c\land d)\lor  (a\land
b\land c\land \lnot d)$$



\begin{enumerate}
\item L'\'{e}criture pr\'{e}c\'{e}dente est-elle une \'{e}criture
disjonctive ? conjonctive ?

\item Mettre $f$ { sous forme normale disjonctive puis
sous forme normale conjonctive.}
\end{enumerate}
\end{exercice}


\begin{exercice}
Donner l'\'{e}criture normale disjonctive puis conjonctive de toutes les
fonctions bool\'{e}\-ennes de 2 variables. On remarquera n\'{e}anmoins que
la fonction nulle n'admet pas d'\'{e}criture normale disjonctive.
\end{exercice}


\begin{exercice}\label{toto}
  Écrire les formules suivantes  sous forme normale disjonctives et dire
  s'il s'agit de tautologies:
  \begin{multicols}{2}
    \begin{enumerate}
    \item $p\land q\land r\limp p\lor q$
\item $((p\limp q)\land (q\limp r))\limp (p\limp r)$
\item $(p\limp q)\limp p$
\item $(p\lequiv (q\lor r))\limp (\lnot q \limp p\lor r)$
    \end{enumerate}
  \end{multicols}
\end{exercice}




\begin{exercice}[Machine à voter]
Le  gouvernement syldave  est constitué  de trois  membres  qui prennent
toutes les décisions en votant  à bulletins secrets. Une proposition est
adoptée lorsqu'elle reçoit au moins deux votes sur trois. Leur conseiller
technique, ancien  étudiant de  l'IUT de Nantes,  leur propose  un petit
circuit qui détermine si une décision est adoptée. 

On note  $x$, $y$  et $z$ les  variables booléennes qui  correspondent à
chacun  des  votes  du  triumvirat. Déterminer  une  fonction  booléenne
$f(x,y,z)$ qui réponde au  problème et dessiner le circuit correspondant
avec les portes NOT, AND et OR.
\end{exercice}




\begin{exercice}[Demi-additionneur]
  On veut additionner deux nombres binaires de un bit. La sortie sera
  double: une  variable $u$ contiendra l'\og unité\fg{}  et une variable
  $r$ contiendra la \og retenue\fg{}. Dresser un tableau puis dessiner
  un circuit ayant deux sorties avec les portes NOT, AND et OR.
\end{exercice}


\begin{exercice}[Divisibilité booléenne]
  Pour  représenter  les  nombres  en  base 2,  on  va  utiliser  quatre
  variables booléennes $b_3$, $b_2$, $b_1$, $b_0$ correspondant chacune aux bits
  de poids décroissants. 
Par   exemple,    $\langle   11\rangle_{10}=\langle1011\rangle_2$   sera
représenté par $b_3=1$, $b_2=0$, $b_1=1$ et $b_0=1$.
Déterminez  l'expression  d'une  fonction  booléenne qui  est  vraie  si
$\langle b_3b_2b_1b_0\rangle_2$ est divisible par 4 ou 5. Vous donnerez votre
réponse sous fnc ou fnd.

\end{exercice}




\begin{exercice}[Système complet]
Sachant  que $\bigl\{\lnot,\land,\lor\bigr\}$  est un  scc,  montrez que
$\bigl\{\lnot,\limp\bigr\}$ est lui aussi un  scc (ce qui sera utile pour
le système  formel de \textsc{Lukasiewicz} (philosophe  polonais (1878 -
1956))...).
$\{\land,\lor\}$ est-il un scc?
\end{exercice}




\begin{exercice}[arbre]
  Donnez les arbres de construction des formules suivantes:
  \begin{multicols}{2}
    \begin{enumerate}
    \item $\lnot(\lnot(x\limp y))\lor\lnot x\limp\lnot y$
\item $(((\lnot x\limp y\land z)\lequiv t)\limp\lnot x\land
      z)\lequiv\lnot -y\land t$
    \end{enumerate}
  \end{multicols}
\end{exercice}



\begin{exercice}[arbres]
  Dressez les  différents arbres  correspondant aux formules  obtenues à
  partir de $a\limp b\limp c\limp d$ en appliquant des parenthésages distincts.
\end{exercice}




\begin{exercice}[Étude syntaxique et sémantique]
  Remplacez  les   ?  par  $\vdash$  et   $\models$  après  vérification
  (préciser le type de la vérification):

  \begin{multicols}{3}
    \begin{enumerate}
    \item $p\limp q \ ? \ q\limp p$
\item $(p\lor r)\limp q \ ? \ p\lor q$
\item $p\limp \lnot q, \lnot r \limp p \ ? \ q\limp r$
    \end{enumerate}
  \end{multicols}
\end{exercice}



\begin{exercice}[théorème de déduction]
  En employant le théorème de déduction, dites si les raisonnements
  suivants sont corrects (pensez à employer des arbres):


  \begin{multicols}{3}
    \begin{enumerate}

\item $
  \begin{array}{c}
    a\limp \lnot b\lor c\\
b\limp a\land \lnot c\\
\hline
c\limp b
  \end{array}
$

\item $
  \begin{array}{c}
 \lnot a \limp b\\
c\limp \lnot a\\
\hline
\lnot a\limp (\lnot c\limp b)
  \end{array}
$


\item 
$
\begin{array}{c}
  p\limp r\land t\\
t\lor s\limp\lnot q\\
\hline
\lnot(p\land q)
\end{array}
$



\item 

$
\begin{array}{c}
  (s\limp r)\land p\\
q\\
\hline
\lnot r\land \lnot s\land p
\end{array}
$










    \item $
      \begin{array}{c}
        p\limp q\land r\\
        r\oplus s\\
\hline
p\limp s\lor t

      \end{array}
$
\item 
$
\begin{array}{c}
  x \lor y \limp z\\
z\lequiv t\\
\hline
x\lor t\limp \lnot y
\end{array}
$
    \end{enumerate}
    
  \end{multicols}
\end{exercice}




\begin{exercice}[Chaînages avant-arrière]

Vous allez  voir votre médecin  en espérant qu'il  a suivi des  cours de
logique.

Voici la situation:
\begin{itemize}
\item  Les  gens qui  ont  la maladie  de  Schplurz  doivent prendre  le
      médicament Xlurbix;
\item Les gens qui ont de la fièvre et des poils qui poussent au fond de
      la gorge ont la maladie de Schplurz;
\item  Ceux qui  ont  une température  supérieure  à 38\textdegree{}  sont
      considérés comme ayant de la fièvre;
\item  Vous  avez  des  poils   dans  la  gorge  et  39,5\textdegree{}  de
      température.
\end{itemize}

Le médecin va-t-il vous prescrire du Xlurbix?
Effectuer un raisonnement sur  des clauses de \textsc{Horn} par chaînage
avant puis par chaînage arrière.
  
\end{exercice}



\begin{exercice}[Police Squad]
C'est bientôt  la fin de l'épisode.  L'inspecteur Franck \textsc{Drebin}
livre   sa   version   des   faits   au  juge   pour   savoir   qui   de
Vincent\textsc{ Ludwig } ou
de Quentin  \textsc{Hapsburg} est le  véritable auteur du meurtre  de la
reine.

\og  \textit{Si Vincent n'a  pas rencontré  Quentin l'autre  nuit, c'est
que  Quentin est  le meurtrier  ou Vincent  est un  menteur.  Si Quentin
n'est pas le meurtrier, alors  Vincent n'a pas rencontré Quentin l'autre
nuit et  le crime a eu  lieu après minuit. Si  le crime a  eu lieu après
minuit,  alors  Quentin  est  le  meurtrier  ou  Vincent  n'est  pas  un
menteur. Donc Quentin est le meurtrier.}\fg{}

Habitué  aux frasques  de l'inspecteur  \textsc{Drebin}, vous  tentez de
réfuter ce raisonnement avec un arbre...

\end{exercice}


\begin{exercice}[Sujet CCP 2011]
  Dans un futur lointain, l'espèce humaine a découvert une autre espèce consciente. L'étude de cette
espèce  a  permis de  découvrir  qu'elle  est  capable de  percevoir  si
quelqu'un dit la vérité ou un mensonge.  Les membres de cette espèce respectent les règles de politesse suivantes lors des discussions
au sein d'un groupe : « Les orateurs doivent rester constants au cours d'une discussion : soit ils disent
toujours la vérité, soit ils mentent toujours. De plus, si un orateur dit la vérité alors l'orateur suivant
doit également dire la vérité. Si le sujet de la discussion change, les orateurs sont libres de changer
leurs comportements. ».


Vous assistez à une discussion sur les moyens d'attaque et de défense que peut posséder la faune de
cette planète entre  trois membres de cette espèce  que nous appellerons
A, B et C.

A : « Le kjalt peut avoir un dard ou des griffes. »

B : « Non, il n'a pas de dard. »

C : « Il a des pinces et des griffes. »

Nous noterons D, G et P les variables propositionnelles associées au fait qu'un kjalt possède respec-
tivement un dard, des griffes et des pinces.

Nous noterons A1 , B1 et C1 les formules propositionnelles associées aux déclarations de A, B et C
dans cette première discussion.

C quitte  le groupe et la discussion  change de sujet pour  parler de la
flore de la planète.

A : « Un lyop peut être de couleur mauve mais pas de couleur jaune. »

B : « Il ne peut pas être de couleur verte. »

A :  « Il ne peut  être de couleur verte  que s'il peut  être de couleur
jaune. »

Nous noterons  J, M  et V les  variables propositionnelles  associées au
fait qu'un lyop peut être respectivement 
de couleur jaune, mauve et verte.

Nous noterons A2 , A3 et B2 les formules propositionnelles associées aux déclarations de A et B dans
cette seconde discussion.

\begin{enumerate}
\item  Représenter les règles de politesse appliquées à la première discussion sous la forme
d'une formule du calcul des propositions dépendant des formules A1 , B1 et C1 .
\item  Représenter les informations données par les participants de la première discussion
sous la forme de formules du calcul des propositions A1 , B1 et C1 dépendant des variables D, G et
P.
\item  En utilisant le calcul des propositions (résolution avec les formules de De Morgan),
déterminer le (ou les) moyen(s) d'attaque et de défense que peut posséder un kjalt.
\item  Représenter les règles de politesse appliquées à la seconde discussion sous la forme
d'une formule du calcul des propositions dépendant des formules A2 , A3 et B2 .
\item  Représenter les informations données par les participants lors de la seconde discussion
sous la forme de trois formules du calcul des propositions A2 , A3 et B2 dépendant des variables J,
M et V .
\item  En utilisant le calcul des propositions (résolution avec les tables de vérité), déterminer
la (ou les) couleur(s) possible(s) pour un lyop.
\end{enumerate}
\end{exercice}

\vfill\eject

\begin{exercice}[Sujet CCP 2008]
Les jeux virtuels sur ordinateur font souvent appel à des énigmes logiques régies par le calcul des
propositions. Vous participez actuellement à une partie dont les règles sont les suivantes:


{\itshape Les propositions composant une énigme sont alternativement vraies et fausses, c'est-à-dire que:
  \begin{itemize}
  \item  soit les  propositions  de numéro pair  sont  vraies et  les
        propositions de numéro impair fausses;
\item soit les propositions de numéro pair sont fausses et les propositions de numéro impair vraies.
  \end{itemize}
}
Dans un labyrinthe, vous vous retrouvez bloqué dans une salle face à une porte sur laquelle se
trouvent deux interrupteurs etiquetés A et B en position ouverte. Sur son seuil figure l'inscription
suivante:

\textit{
Pour ouvrir la porte :
\begin{description}
\item[P1] Il faut fermer l'interrupteur A.
\item[P2] Il faut fermer simultanément les interrupteurs A et B.
\item[P3] Il ne faut pas fermer l'interrupteur B.
\end{description}
Attention, en cas d'erreur la salle s'auto-détruira...
}

\begin{enumerate}

\item  Exprimer P1 , P2 et P3 sous la forme de formules du calcul des propositions dépendant
de A et de B.

\item  Exprimer la règle du jeu dans le contexte des propositions P1 , P2 et P3.

\item  En utilisant le  calcul des  propositions, déterminer  l'action à
       effectuer pour ouvrir la porte.

\item  Les interrupteurs A et B laissent passer un courant (valeur logique vraie) quand ils sont
fermés. Proposer un circuit électronique composé de portes logiques comportant deux sorties O et D.
La sortie O laisse passer le courant pour ouvrir la porte. La sortie D laisse passer le courant pour
détruire la salle.
\end{enumerate}
\end{exercice}

\begin{exercice}[École de l'Air 2004]
  On souhaite concevoir un circuit  logique qui renvoie le nombre modulo
  $2$ de $0$ pr{\'e}sents dans un mot pass{\'e} en entr{\'e}e au circuit
  constitué uniquement de 0 et de 1.

On pourra utiliser les portes logiques {\'e}l{\'e}mentaires \textit{et},
\textit{ou}, \textit{non} et \textit{xor} (ou exclusif).



\begin{enumerate}
\item Commen{\c c}ons par un mot de longueur $1$ : $u= a$, avec $a \in \{0, 1\}$.

Construire un circuit $\mathcal{P}_{0}$ {\`a} une seule entr{\'e}e $a$ et une sortie $s$ qui vaut $0$ si $u$ contient un nombre pair de $0$ et $1$ sinon.

\item Supposons con{\c c}u un circuit $\mathcal{P}_{n}$ qui prend en entr{\'e}e un mot $u$ de longueur $2^{n}$ et poss{\`e}de une sortie $s$ qui vaut $0$ si $u$ contient un nombre pair de $0$ et $1$ sinon.

Construire,    {\`a}   l'aide    de   $\mathcal{P}_{n}$,    un   circuit
$\mathcal{P}_{n+1}$ qui r{\'e}sout le  m{\^e}me probl{\`e}me pour un mot
de longueur $2^{n+1}$ en entr{\'e}e.

\end{enumerate}

\end{exercice}



\begin{exercice}[Politique Bordure]

Grand meeting  du PUB,  Parti Unique Bordure,  afin de  choisir l'unique
candidat des futurs élections dictatoriales.

Deux  candidats sont  en lice:  Josef  Chrtzw et  Nikalaï Schrpuntz.  Un
premier orateur intervient:

{\itshape Dieter de Villenstein: \og{} Il faut soutenir Josef Chrtzw.  Et
soutenir l'action de  M. Chrtzw, ce n'est pas ne  pas soutenir notre ami
à tous: Nikalaï Schrpuntz\fg{}.}

La réponse du deuxième candidat:

{\itshape Nikalaï Schrpuntz: \og  Je n'ai qu'une seule ambition: l'unité
de notre parti unique. C'est  pourquoi, mes chers camarades, me soutenir
à la direction  du PUB, c'est soutenir l'action de  notre modèle à tous,
Josef Chrtzw \fg{}}.

Finalement, les militants du PUB ont élu Nikalaï Schrpuntz avec 99\% des voix.

Traduisez en logique des  propositions les déclarations des candidats et
la conclusion des militants.
Vous utiliserez les propositions atomiques suivantes:
\begin{itemize}
\item S: soutenir Nikalaï Schrpuntz;
\item C: soutenir Josef Chrtzw;
\item V: Villenstein est un menteur;
\item SM: Nikalaï Schrpuntz est un menteur.
\end{itemize}

Le raisonnement des militants est-il valide?

  
\end{exercice}










\subsection*{Un peu de CAML...}


\subsubsection*{Les types}

On crée un  type construit récursif pour les formules  avec un type pour
les atomes à choisir au départ.  On prendra ici des entiers pour plus de
faciliter de programmation.


\caml

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


Par exemple, quelle formule représente:

\begin{lstlisting}[caption={}]
Equiv(Non(Et(Atomic 0,Atomic 1)) , Ou(Non(Atomic 0),Non(Atomic 1)))
\end{lstlisting}

Donnez l'arbre syntaxique associé.

C'est peu lisible malgré tout...
Je vous donne dans ma grande bonté un début de petite fonction récursive
qui va faciliter la lecture:


\begin{lstlisting}[caption={}]
let rec dit_formule formule = match formule with
  |Faux -> "Faux"
  |Non Faux -> "Vrai"
  |Atomic a -> string_of_int a
  |Non p -> "non " ^ dit_formule p
  |Et(p,q) -> "( " ^ dit_formule p ^ " et " ^ dit_formule q ^ " )"
...
\end{lstlisting}


Par exemple:

\begin{lstlisting}[caption={}]
# dit_formule ( Implique(Et(Atomic 2,Non Faux),Non (Ou(Faux,Atomic 3))) );;
- : string = "( ( 2 et Vrai ) implique non ( Faux ou 3 ) )"
\end{lstlisting}

\subsubsection*{Approche sémantique}


Un  environnement  sera modélisé  sur  \textsc{Caml}  par  une liste  de
booléens.

Pour calculer  la valeur booléenne  d'une formule sous  un environnement
donné \texttt{f}, on va procéder ainsi:

\begin{itemize}
\item la constante \texttt{Faux} sera associée à \texttt{false};
\item un atome \texttt{a} sera associé à sa valeur dans l'environnement,
      c'est-à-dire renverra l'élément en position \texttt{a} de la liste
      \texttt{f} (d'où l'intérêt de  travailler avec des entiers mais on
      aurait pu contourner le problème...);
\item si $p$  est une formule, la valeur de sa  négation est la négation
      booléenne de sa valeur;
\item etc.
\end{itemize}

Il faudra  donc disposer  tout d'abord d'une  fonction \texttt{  nieme k
liste} qui renvoie le $k$\eme élément de la liste \texttt{liste}.

\begin{lstlisting}[caption={}]
exception Mauvais_numero;;

let rec nieme k liste =
  match liste with
    |[] -> raise Mauvais_numero
    |t::q -> if... then ...
      else ...;;
\end{lstlisting}

\begin{lstlisting}
# nieme 3 [1;2;3;4;5];;
- : int = 3
\end{lstlisting}

On  abusera  du  \texttt{if}...\texttt{then}...\texttt{else}....  et  on
utilisera certaines équivalences:


\begin{lstlisting}[caption={}]
let rec eval formule env =
  match formule with
    |Faux -> false
    |Atomic a -> nieme a env
    |Non p -> if (eval p env) then false else true
    |Et (p,q) ->
      if (eval p env) then
	if (eval q env) then
	  true
	else
	  false
      else

...
\end{lstlisting}


Ensuite, il faudra tester si une formule est une tautologie.

Pour  cela,  il faudrait  créer  la  liste  de tous  les  environnements
possibles. On a besoin de quelques outils sur les listes:

\begin{itemize}
\item \texttt{concat l1 l2} qui concatène les deux listes \texttt{l1} et
      \texttt{l2}.
\item \texttt{ ajoute\_el el liste\_de\_listes} qui fait ça:

  \begin{lstlisting}[caption={}]
let rec ajoute_el el liste_de_listes =
  match liste_de_listes with
    |[] -> []
    |t::q -> (el::t)::(ajoute_el el q);;
  \end{lstlisting}

Ça fait quoi au juste?
\end{itemize}

Ensuite on cherche tous les environnements de longueur n. Par exemple:

\begin{lstlisting}[caption={}]
# tous_environnements 3;;
- : bool list list =
[[true; true; true]; [true; true; false]; [true; false; true];
 [true; false; false]; [false; true; true]; [false; true; false];
 [false; false; true]; [false; false; false]]
\end{lstlisting}

Il ne reste  plus qu'à évaluer une formule  sous tous ces environnements
pour savoir si c'est une tautologie.


\begin{lstlisting}[caption={}]
# let est_tautologie formule n =
...
val est_tautologie : formule -> int -> bool = <fun>
# est_tautologie ( Equiv(Non(Et(Atomic 0,Atomic 1)) , Ou(Non(Atomic 0),Non(Atomic 1)))) 2;;
- : bool = true
\end{lstlisting}


Testez vos résultats sur l'\vref{toto}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\end{listeexercices}
\modenormal % restaure les définitions de sections, sous-sections, etc.

%%% Local Variables: 
%%% TeX-master: "Poly_ERCB_2012"
%%% End: 
