<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">% AG. Sur ce sujet voir GochetGribomont et [Fitting90].

\subsection{Tableaux de Beth}
Il s'agit d'une autre méthode de démonstration formelle, ignorant 
tout système d'axiomes, mais comportant de nombreuses règles 
d'inférence, également appelée méthode des tableaux sémantiques.

Elle est particulièrement adaptée à l'automatisation des 
démonstrations, et constitue une ouverture sur les algorithmes 
étudiés en seconde année (utilisation systématique du \og théorème de 
falsification\fg{}  qui sera envisagé plus loin).\psaut

\subsubsection{Principe de la méthode}

Il s'agit de montrer qu'une formule $F$ est un théorème( $\theor F$); 
le résultat est obtenu en montrant que la \og réfutation\fg{}  de $F$ 
conduit à une contradiction.

La \og réfutation\fg{}  se conduit dans un arbre (appelé tableau de 
Beth (logicien néerlandais). \og Réfuter\fg{}  $F$, c'est le \og 
nier\fg{}, selon sa forme, en suivant les règles d'inférences qui 
sont données dans le tableau :\gsaut

% \centerline{\begin{tabular}{|c|c|}
% \noalign{\hrule}
% Règles d'affirmation &amp; Règles de réfutation
% \noalign{\hrule} \\
% $\begin{array}{c}\tvii{15}\non A \cr\sur A \cr \end{array}$
% &amp;
% $\begin{array}{c} \tvii{15}\sur{\non A} \cr A \cr \end{array}$
% \noalign{\hrule}\\
% $\begin{array}{c} \tvii{15}A\ou B \cr \swarrow\searrow \cr A\qquad B\cr \end{array}$
% &amp;
% $\begin{array}{c} \tvii{15}\sur{A\ou B} \cr \sur A \cr \sur B \cr \end{array}$
% \noalign{\hrule}\\
% $\begin{array}{c} \tvii{15}A\et B \cr A \cr B \cr \end{array}$
% &amp;
% $\begin{array}{c} \tvii{15}\sur{A\et B} \cr \swarrow\searrow \cr \sur A\qquad\sur B \cr
% \end{array}$
% \noalign{\hrule}\\
% $\begin{array}{c} \tvii{15}A\imp B \cr \swarrow\searrow \cr \sur A\qquad B\cr \end{array}$
% &amp;
% $\begin{array}{c} \tvii{15}\sur{A\imp B} \cr A \cr \sur B
%   \cr \end{array}$
% \noalign{\hrule}
% \end{tabular}}



La règle de contradiction est 
\begin{tabular}{|c|}\noalign{\hrule}$A$\\$\sur A$\\$\clv$\\
\noalign{\hrule}\end{tabular}\ .\gsaut


\'Ecrire, dans un tableau de Beth, $A$ signifie \og j'affirme 
$A$\fg{}  et $\sur A$ signifie \og je nie $A$\fg{}  (ne pas confondre 
avec $\non A$).


Une branche d'un tableau de Beth est considérée comme terminée 
lorsque plus aucune règle ne peut s'appliquer et elle est considérée 
comme close lorsqu'elle contient le symbole de contradiction $\clv$.

Il n'est pas nécessaire, pour l'application de la règle de 
contradiction, que $A$ et $\sur A$ figurent dans cet ordre, ni même 
consécutivement, dans l'arbre : il suffit qu'ils soient dans la même 
branche.

\subsubsection{Justification de la méthode}

Le théorème suivant fonde cette méthode :\saut

\begin{Th}[Théorème de Beth]
\index{théorème!de Beth}
La formule $F$ est un théorème si et seulement si $\sur F$ est la 
racine d'un arbre dont toutes les branches sont closes.
\end{Th}



\subsubsection{Exemple}

Démonstration de $\theor ((P\imp Q)\imp P)\imp P$\saut 
$$\begin{array}{|c|c|}
\noalign{\hrule}
\multicolumn{2}{|c|}{\tvii{15}\sur{((P\imp Q)\imp P)\imp P}}\cr
\noalign{\hrule}
\multicolumn{2}{|c|}{\tvii{15}\sur P}\cr
\noalign{\hrule}
\multicolumn{2}{|c|}{\tvii{15}(P\imp Q)\imp Q}\cr
\noalign{\hrule}
\tvii{15}\sur{P\imp Q} &amp;  P\cr
\noalign{\hrule}
\tvii{15}  P      &amp;        \clv\cr
\noalign{\hrule}
\tvii{15} \sur Q &amp; \cr
\noalign{\hrule}
\tvii{15}  \clv &amp; \cr
\noalign{\hrule}
\end{array}$$
</pre></body></html>