partie4.tex

%% Partie 4 commence ici
% Cette partie n'est plus utilisée, car fusionnée avec partie 3

% \section{Deux règles plus sophistiquées}
% \subsection{Théorème de déduction}
% 
% \begin{itemize}
% \item  Pour prouver s $\Rightarrow$ t
% \item  On suppose s vrai
% \item  On déduit t
% \item  Ensuite, on évacue l'hypothèse
% \end{itemize}
% 
% 
% \textit{Notation: p $\vdash$ t (on peut prouver t à partir de p) }
% 
% \subsubsection{Prémisse:}
% 
% \begin{equation}
% \frac{p,..., r, s \vdash t} 
% {p,..., r \vdash (s \Rightarrow t)}
% \end{equation}
% 
% \subsubsection{Conclusion:}
% 
% Déduire une implication
% 
% \subsection{Preuve par contradiction (ou preuve indirecte)}
% 
% On prend une hypothèse, et on peut prouver qu'elle est vraie ou fausse, d'où l'hypothèse n'est pas bonne.
% 
% \subsubsection{Prémisse:} 
% on suppose que p...q n'a pas de problème
% 
% \begin{equation}
% \begin{split}
% p,...,q, r, s \vdash s \\
% \frac{p,...,q, r, s \vdash \lnot s}
% {p,...,q \vdash \lnot r}
% \end{split}
% \end{equation}
% 
% \subsubsection{Conclusion:}
% 
% si p...q n'a pas de problème, on se focalise alors sur r

\section{Exemples de l'utilisation des schémas}

Pour illustrer l'utilisation des deux schémas, la preuve conditionnelle et la preuve par contradiction,
nous allons prouver la même conclusion en trois manières, avec chaque schéma et sans schéma.
\begin{itemize}
\item Prémisse: $(p \land q) \lor r$
\item Conclusion: $\lnot$ p $\Rightarrow$ r
\end{itemize}

\subsection{Exemple sans schéma}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r$ & \textit{Prémisse} \\
2. $r \lor (p \land q)$ & \textit{Commutativité en 1} \\
3. $(r \lor p) \land (r \lor q)$ & \textit{Associativité en 2}\\
4. $(r \lor p)$ & \textit{Simplification en 3}\\
5. $(p \lor r)$ & \textit{Commutativité en 4}\\
6. $\lnot \lnot p \lor r $ & \textit{Loi de la négation en 5}\\
7. $\lnot p \Rightarrow r $ & \textit{Implication en 6}\\
\hline
\end{tabular}

\subsection{Exemple de preuve conditionnelle}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r $ & \textit{Prémisse} \\
2. $\lnot \lnot(p \land q) \lor r $ & \textit{Double négation en 1} \\
3. $\lnot ( \lnot p \lor \lnot q) \lor r $ & \textit{Loi De Morgan en 2} \\
4. $\lnot p \lor \lnot q \Rightarrow r $ & \textit{Implication en 3}\\
\indent 5.  $\lnot p $ & \textit{Hypothèse}\\
\indent 6.  $\lnot p \lor \lnot q $& \textit{ Addition sur 5}\\
\indent 7.  $r$ & \textit{ Modus Ponens sur 4 et 6}\\
8.  $\lnot p \Rightarrow r $& \textit{Evacuation de l'hypothèse}\\
\hline
\end{tabular}

\subsection{Exemple de preuve par contradiction}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r $ & \textit{Prémisse}\\
2. $ (p  \lor r) \land (q \lor r)$ & \textit{Distributivité sur 1}\\
3. $(p \lor r)$ & \textit{Simplification en 2}\\

 \indent 4. $\lnot ( \lnot p \Rightarrow r)$ & \textit{Hypothèse}\\
 \indent 5. $\lnot ( \lnot \lnot p \lor r)$ &\textit{Implication en 4}\\
 \indent 6. $\lnot (p \lor r)$ & \textit{ Négation en 5}\\


7. $\lnot \lnot (\lnot p \Rightarrow r) $ & \textit{ Preuve par contradiction}\\
8. $\lnot p \Rightarrow r $ & \textit{Négation en 7}\\
\hline
\end{tabular}


\section{Quelques concepts supplémentaires}
\subsection{Principe de dualité }

\subsubsection{Dans les formules sans $\rightarrow$ :}

\begin{align*}
\land \leftrightarrow \lor \\ 
true \leftrightarrow false 
\end{align*}
\begin{align*}
\models \lnot ( p \land q)  \Leftrightarrow \lnot p \lor \lnot q \\
\models \lnot ( p \lor q)  \Leftrightarrow \lnot p \land \lnot q 
\end{align*}

\subsubsection{Formule quelconque:}

\begin{align*}
\land \leftrightarrow \lor \\ 
true \leftrightarrow false \\ 
p \leftrightarrow \lnot p 
\end{align*}

 Justification en raisonnant sur les modèles:
 \begin{align*}
	 (p_1,...,p_n) \models q \hspace{1cm} ssi \models (p_1 \land ... \land p_n \land q) \leftrightarrow false \\
	 ssi \models ( \lnot p_1 \lor ... \lor \lnot p_n \lor q) \leftrightarrow true
 \end{align*}



\subsection{Algorithme de normalisation}

Une formule quelconque peut être transformée en une formule équivalente de forme normale.

\subsubsection{Forme Normale}

\begin{itemize}
  \item Conjonctive: $( p \lor q ) \land ( q \lor a ) \land ( s \lor r )$  
  \item Disjonctive: $( p \land q ) \lor ( q \land a ) \lor ( s \land r )$  
\end{itemize}

\subsubsection{Terminologie}

\begin{itemize}
	\item Littéral : $P \lor \lnot P \approxeq L$
	\item Clause : $\lor L_i = ( L_1 \lor L_2 \lor L_3 \lor ... \lor L_i )$
\end{itemize}

\subsubsection{Algorithme de normalisation}

\begin{enumerate}
\item Eliminer les $\rightarrow$ et $\leftrightarrow$
\item Déplacer les négations vers l'intérieur (dans les propositions premières) De Morgan
\item Déplacer les disjonctions ($\lor$) vers l'intérieur
\item Simplifier $(P \lor \lnot P)$
\end{enumerate}

\subsubsection{Exemple de normalisation}

\begin{align*}
& (p \rightarrow (Q \rightarrow R)) \rightarrow ((P \land S) \rightarrow R) \\
& \lnot ( ... ) \lor ( ... ) \\
& \lnot (\lnot P \lor (\lnot Q \lor R)) \lor (\lnot (P \land S) \lor R) \\
& ( \lnot \lnot P \land \lnot (\lnot Q \lor R)) \lor ((\lnot P \lor \lnot S) \lor R) \\
& (P \land (Q \land \lnot R)) \lor ( \lnot P \lor \lnot S \lor R) \\
& (P \lor \lnot P \lor \lnot S \lor R) \land ( Q \lor \lnot P \lor \lnot S \lor R) \land (\lnot R \lor \lnot P \lor \lnot S \lor R) \\
& (Q \lor \lnot P \lor \lnot S \lor R) 
\end{align*}