\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Un syllogisme d'Aristote}
\begin{itemize}
  \item Tous les hommes sont mortels. Socrate est un homme. 
  Donc \pause Socrate est mortel.
  \item \pause Comment formaliser ce raisonnement en logique des
  propositions ?
  \item \pause ``Tous les hommes sont mortels'' est une
  propriété générale \pause (on ne peut pas énumérer tous les êtres
  vivants, même pas tous les hommes)
  \item \pause On introduit
  \begin{itemize}
    \item des variables ($x$, $y$, \ldots), à valeur dans
    un ``univers (des objets) du discours''
    \item \pause des propriétés générales :
            $H(x)$ pour ``$x$ est un homme'', 
      $M(y)$ pour \pause ``$y$ est mortel''
    \item \pause une notation pour les propriétés universelles :
        \pause $ \forall x .\, H(x) \pause \Rightarrow M(x) $
  \end{itemize} 
  \item $H$ et $M$ sont des prédicats (unaires)
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Exercice}
\begin{itemize}
  \item Formaliser les phrases suivantes en logique des prédicats
  \begin{enumerate}
  \item Tous les étudiants travaillent les mathématiques
  \item Pierre travaille la physique
  \item Le fils de Pierre travaille les mathématiques
  \item Tous les étudiants travaillent au moins une matière 
  \item Il y a au moins une matière travaillée par tous les étudiants
  \end{enumerate}
  \item \pause Réponses
  \begin{enumerate}
  \item $\forall x .\, $ travaille(x,Maths)
  \item \pause travaille(Pierre, Physique)
  \item \pause travaille(fils(Pierre),Maths)
  \item \pause $\forall x .\, \exists y.\,$  travaille$(x,y)$
  \item \pause $\exists y.\, \forall x .\,$  travaille$(x,y)$
  \end{enumerate}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Langages du premier ordre}
\begin{itemize}
\item Un \emph{langage du premier ordre} est défini par un ensemble
infini $X$ de variables et deux ensembles finis de symboles :
\begin{itemize}
  \item une signature fonctionnelle $F$ de symboles fonctionnels
  d'arité fixée
  \item une signature relationnelle $R$ de symboles
  relationnels d'arité fixée
\end{itemize}
\item \pause Les sous-ensembles de symboles fonctionnels et
relationnels d'arité $n$ sont notés $F_n$ et $R_n$
\item \pause Un \emph{terme} est soit une variable, soit un symbole
fonctionnel d'arité $n$ ($n \geq 0$) appliqué à $n$ termes 
\item \pause Un \emph{atome} (ou \emph{formule atomique}) est un
symbole relationnel d'arité $n$ ($n \geq 0$) appliqué à $n$ termes
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Exercice 2 (partie I.9 du support de cours)}
$f^n$ signifie que le symbole $f$ (fonctionnel ou
relationnel) est d'arité $n$.
On considère un langage 
$\mathcal{L}$ de signature fonctionnelle 
$\{f^1, g^1, h^2\}$ et de signature relationnelle 
$\{ R^1, S^2, T^2, =^2\}$.
On considère les expressions suivantes :
\begin{itemize}
\item 
$ \varphi_1  : 
\exists x \,. \, 
(
(\forall y \, . \, 
(\exists z \,.\,
R(x)))) \lor
(\exists y \, .\, 
(\neg 
(\forall z \, . \, 
(S(h(x,z)x)))))
$

\item $ \varphi_2  : (\forall x \, .\, (T(f(x),y)) \imp (\neg (\exists
x \, .\, (f(x,y)))))$

\item $ \varphi_3  : (\forall z \, .\, T(x,y) \imp (\exists y \,.\,
((\forall x '\neg (f(x) = y))) \lor T(y,z)))$

\item $ \varphi_4  : (\forall x \,.\, (\exists y  \,.\, (( g(y) = x)
\lor (\neg T(y,y))))) \imp (\exists y \,.\, (\forall x \,.\,
(T(y,g(x)))))$
\end{itemize}

\begin{enumerate}
\item Parmi ces expressions, lesquelles sont des formules de
$\mathcal{L}$ ?
\item Dans celles qui sont des formules, supprimer les parenthèses
  inutiles
\item Déterminer les occurrences liées des variables dans les formules
\end{enumerate}
\end{frame}

\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Types des termes et des formules}
En Objective Caml

\textsf{type term =}

\textsf{    Var of string}
    
\textsf{  $|$ Terme of string * term list;;}
  
\textsf{type pred =}
 
\textsf{    Vrai}
    
\textsf{  $\mid$ Faux}
   
\textsf{  $\mid$ Atome of string * term list}
   
\textsf{  $\mid$ Neg of pred}
   
\textsf{  $\mid$ Ou of pred * pred}
   
\textsf{  $\mid$ Et of pred * pred}
  
\textsf{  $\mid$ Imp of pred * pred}
  
\textsf{  $\mid$ Equiv of pred * pred}
  
\textsf{  $\mid$ PourTout string pred}
  
\textsf{  $\mid$ Existe string pred;;}
\end{frame}

\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Exercice 3}
On considère un ensemble d'objets de différentes couleurs.
Chacun de ces objets porte un numéro et possède une forme géométrique
particulière (cube, sphère prisme).
En utilisant les prédicats 
$\textit{pair}(x)$, $\textit{cube}(x)$,
    $\textit{vert}(x)$, \ldots codez les phrases suivantes :
\begin{enumerate}
\item Si un objet est sphérique, alors cet objet n'est pas vert ou
  porte un numéro impair.
\item S'il existe un objet vert sphérique, alors il existe un objet
  vert portant un numéro impair.
\item Si tout objet vert porte un numéro impair, alors aucun objet
  sphérique n'est vert.
\end{enumerate}
\end{frame}

% Ces diapos font aussi office de support de cours
\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Objectif}
\begin{itemize}
  \item Soit $\varphi$ une formule d'un langage du premier ordre
  \item \pause Par exemple, $\varphi$ peut être
 $$(\forall y \, . \, 
      (\exists z \,.\, R(z))
     \lor
      (\forall z \, . \,  S(y,z) \land \neg S(h(x,z),a))
 )$$
  \item \pause Quand peut-on dire que la formule $\varphi$ est vraie ?
  \item \pause La vérité de $\varphi$ dépend 
  \begin{itemize}
    \item du sens des symboles fonctionnels 
    \pause ($a$ et $h$ dans l'exemple) et relationnels 
    \pause ($R$ et $S$ dans l'exemple)
    
    \pause $\rightarrow$ notion d'\emph{interprétation}
    
    \item de la valeur des variables libres de $\varphi$
         \pause ($x$ dans l'exemple)  
    
    \pause $\rightarrow$ notion d'\emph{environnement}
  \end{itemize}
  \item Globalement, il s'agit de définir la \emph{sémantique} (le
  sens, la signification) d'un langage du premier ordre
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Définition d'une interprétation}
Une \emph{interprétation} $\mathcal{I}$ d'un langage $L$ du premier
ordre consiste à choisir
\begin{itemize}
   \item un ensemble non vide $\mathcal{U}_{\mathcal{I}}$, appelé
   \emph{domaine d'interprétation}, ou univers
   \item \pause une fonction $f_{\mathcal{I}}$ de
   ${\mathcal{U}_{\mathcal{I}}}^n$ dans $\mathcal{U}_{\mathcal{I}}$
   pour chaque symbole fonctionnel $f$ d'arité $n$ de $L$
   \item \pause une relation $R_{\mathcal{I}}$ sur
   ${\mathcal{U}_{\mathcal{I}}}^n$ pour chaque symbole relationnel $R$
   d'arité $n$ de $L$
\end{itemize}
\pause L'ensemble $\mathcal{U}_{\mathcal{I}}$, muni de
ses fonctions  $f_{\mathcal{I}}$ et de ses relations
$R_{\mathcal{I}}$ est appelé \emph{structure} (interprétative)
\end{frame}

\begin{frame}
\frametitle{Interprétation}
\framesubtitle{Exemple}
\begin{itemize}
   \item $\mathcal{U}_{\mathcal{I}} = \mathbb{Z}$
   \item $a_{\mathcal{I}} = -1$
   \item $h_{\mathcal{I}}(x,y) = x + y$
   \item $R_{\mathcal{I}} =$ ``$\leq 0$''
   \item $S_{\mathcal{I}} =$ ``$>$''
   \item $(\mathbb{Z}, -1, +, \leq 0, >)$ est une structure
   interprétative
\end{itemize}   
\pause \noindent Exercice
\begin{enumerate}
  \item Traduire en français ce que signifie $\varphi$ dans
   cette structure 
   \item
   \pause Pour quelles valeurs de $x$ la formule $\varphi$ est-elle
   vraie dans cette structure ?
\end{enumerate} 
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Définition d'un environnement}
\begin{itemize}
 \item Soit $L$ un langage
 du premier ordre, $\mathcal{I} = (\mathcal{U}_{\mathcal{I}}, \ldots)$ une
 interprétation de $L$ et $\varphi$ une formule de $L$
 \item \pause La vérité de la formule $\varphi$ dans l'interprétation
 $\mathcal{I}$ ne dépend que de la valeur de ses
 variables libres dans le domaine d'interprétation
 \pause $\hookrightarrow$ pour la définir, on introduit la notion
 suivante
 \item 
 Un \emph{environnement} (ou ``assignation'', ou ``affectation'')
 du langage $L$ est le choix d'une valeur dans le domaine
 d'interprétation pour chaque variable de l'ensemble $X$ des variables
 de $L$
 \pause
 \begin{itemize}    
 \item Formellement, un environnement est une fonction (totale) $e$
 de $X$ dans $\mathcal{U}_{\mathcal{I}}$
 \item La vérité de $\varphi$ dans l'interprétation
 $\mathcal{I}$ ne dépend que de $e$ 
 \item Dans l'environnement $e$, on doit définir successivement la
 \emph{valeur} de tout terme $t$, puis la valeur de vérité de
 toute formule
 \end{itemize}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Définition de la valeur d'un terme}
Dans une interprétation $\mathcal{I}$ donnée, la valeur 
$\textit{val}_{\mathcal{I}}(t,e)$ du terme $t$ dans l'environnement $e$ est définie
comme suit
\begin{itemize}
  \item Si $x \in X$ est une variable, alors $\textit{val}_{\mathcal{I}}(x,e) = $
  \pause $e(x)$ 
  \item \pause 
  Si $f$ est un symbole fonctionnel d'arité $n$ $(n \geq 0)$ et si
  $t_1, \ldots, t_n$ sont $n$ termes, alors
  
  $\textit{val}_{\mathcal{I}}(f(t_1, \ldots, t_n),e) =$ \pause
  $f_{\mathcal{I}}(\textit{val}_{\mathcal{I}}(t_1,e), \ldots, \textit{val}_{\mathcal{I}}(t_n,e))$
\end{itemize}
\pause C'est une définition récursive car les termes sont eux-mêmes
définis de manière récursive (sera approfondi dans le cours sur
les types inductifs)    
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Défnition de la valeur de vérité d'une formule}
Soit $L$ un langage du premier ordre, $\mathcal{I}$ une interprétation
de $L$, $\varphi$ une formule de $L$ et $e$ un environnement de $L$. La
\emph{valeur de vérité} de la formule $\varphi$ dans l'environnement
$e$ est la constante booléenne 0 ou 1 notée
$\textit{eval}_{\mathcal{I}}(\varphi,e)$ et définie comme suit
\begin{eqnarray*}
 \textit{eval}_{\mathcal{I}}(R(t_1,\ldots,t_n),e) & = & 1 
  \textrm{ ssi } 
 \pause 
 (\textit{val}_{\mathcal{I}}(t_1,e), \ldots, 
  \textit{val}_{\mathcal{I}}(t_n,e)) \in
   R_{\mathcal{I}} \\
 \pause
 \textit{eval}_{\mathcal{I}}(\neg F,e) & = & 
 \pause
 \overline{\textit{eval}_{\mathcal{I}}(F,e)}  \\ 
 \pause 
 \textit{eval}_{\mathcal{I}}(F \vee G,e) & = &
  \pause \textit{eval}_{\mathcal{I}}(F,e) \ +  \
  \textit{eval}_{\mathcal{I}}(G,e)  \\
 \pause
  \textit{eval}_{\mathcal{I}}(\forall x \,.\, F,e) & = & 1 
 \textrm{ ssi } 
 \pause 
 \textit{eval}_{\mathcal{I}}(F,e [x \mapsto u]) = 1
 \textrm{ pour tout } u \in \mathcal{U}_{\mathcal{I}}\\
 \ldots
\end{eqnarray*}
\pause où $e[x \mapsto u]$ est l'environnement défini à partir de $e$
 par $$e[x \mapsto u](y)=\left\{ \begin{array} {ll} e(y) &
 \text{si}~ y \not = x\\
    u & \text{si} ~ y = x \end{array}\right.$$

\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Valeur de vérité d'une formule}
\noindent Questions de compréhension
\begin{enumerate}
 \item Préciser ce que sont $R$, $n$, $t_1$, 
  \ldots, $t_n$, $F$, $G$ et $x$ dans cette définition  
 \item \pause Compléter la définition avec les cas des connecteurs
  logiques $\land$, $\Rightarrow$, $\Leftrightarrow$, \ldots
 \item \pause Compléter la définition avec le cas du
 quantificateur $\exists$
 \item \pause Appliquer cette définition étape par étape à la formule 
 $$(\forall y \, . \, 
      (\exists z \,.\, R(z))
     \lor
      (\forall z \, . \,  S(y,z) \land \neg S(h(x,z),a))
 )$$
 pour l'interprétation $(\mathbb{Z}, -1, +, \leq 0, >)$ et
 l'environnement qui donne à $x$ la valeur $0$
\end{enumerate}
% Solution 
\end{frame}

% Solution de l'exercice à retoucher
% \begin{eqnarray}
% \textit{eval}_{\mathcal{I}}(F \wedge G) & = & \pause
%  I_v(F) \ .  \ I_v(G) \label{iet} \\
%  \pause
%  \pause \textit{eval}_{\mathcal{I}}(F \Rightarrow G) & = & \pause \textit{eval}_{\mathcal{I}}(\neg F \vee G)
%  \label{iimplique} \\ 
%  \pause \textit{eval}_{\mathcal{I}}(F \Leftrightarrow G) & = & \pause \textit{eval}_{\mathcal{I}}( (F \Rightarrow G)
%  \wedge (G \Rightarrow F))  \label{iequiv}
% \end{eqnarray}
% o\`u $F$ et $G$ sont des formules propositionnelles
 

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Satisfaisabilité et validité}
Dans une interprétation donnée
\begin{itemize}
  \item une formule est dite \emph{valide} si
elle est vraie \pause dans tous les environnements

\item \pause une formule est dite \emph{satisfaisable}
 \pause s'il existe au moins un environnement dans lequel elle est
 vraie
\item \pause une formule est dite \emph{close} si \pause elle n'a pas
de variables libres
\item \pause Soit $x_1, \ldots, x_n$ les variables libres de
$\varphi$
\begin{itemize}
  \item $\forall x_1 \,.\, \ldots \forall x_n \,.\,
\varphi$ s'appelle la clôture \pause universelle de $\varphi$
\item $\exists x_1 \,.\, \ldots \exists x_n \,.\, \varphi$
s'appelle \pause la clôture existentielle de $\varphi$
\end{itemize}
\item  $\varphi$ est valide ssi sa clôture \pause universelle est
vraie
\item \pause $\varphi$ est satisfaisable ssi \pause sa clôture 
existentielle est vraie
\end{itemize} 
Conclusion ?
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Relation de satisfaction}
Soit $\varphi$ une formule close
\begin{itemize}
\item On dit que 
 \begin{itemize}
  \item ``la structure $\mathcal{S}$ satisfait
$\varphi$'', ou bien que
 \item ``$\mathcal{S}$ est un modèle de $\varphi$''  
 \end{itemize} et on note  $\mathcal{S} \models \varphi$
si la formule $\varphi$ est vraie dans la structure/interprétation 
$\mathcal{S}$ 
\item \pause L'environnement n'intervient pas car la formule est
close
\end{itemize}
\end{frame}

% retour au poly, def 7.10
\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Tautologie, conséquence logique, équivalence}
Soit $C$,  $H_1, \ldots, H_n$, $P$ et $Q$ des formules closes

\begin{itemize}
\item \pause On dit que la formule $C$ est une \emph{tautologie} et on
écrit $\models C$ \pause s'il existe au moins une interprétation
$\mathcal{S}$ telle que $\mathcal{S} \models C$
\item \pause On dit que la formule $C$ est une \emph{conséquence
logique} des formules $H_1, \ldots, H_n$ et on écrit $\{ H_1,
\ldots, H_n \} \models C$ si \pause toutes les interprétations
$\mathcal{S}$ telles que $\mathcal{S} \models H_1$ et \ldots
et $\mathcal{S} \models H_1$ sont telles que $\mathcal{S} \models
C$
\item \pause On dit que les formules $P$ et $Q$ sont (logiquement)
équivalentes et on écrit $P \approx Q$ si \pause $\{ P \} \models Q$
et $\{ Q \} \models P$
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Exercice 4 (partie II.2, trou à compléter)}
$\non (\exi x\, . \, p(x)) \approx (\qqs x \,.\, \non p(x)) $,
$\non (\qqs x \,.\, p(x)) \approx  (\exi x\, . \, \non p(x))$
\begin{itemize}
  \item Appliquer ces équivalences et toutes les équivalences
  propositionnelles connues pour simplifier la négation des formules
  suivantes
\begin{enumerate}
\item  $\forall x \, .\, p(x) \imp q(x)$
\item  $\exists x \, .\, p(x) \land q(x)$
\item  $\forall x \, . \, p(x) \eqv q(x)$
\item  $\exists x\, .\, (\forall y \,.\,
  q(x,y) \imp (p(x,y) \lor r(x,y)))$ 
\end{enumerate}
  \item \pause Réponses \pause
  \begin{enumerate}
\item $\exists x \, .\, p(x) \land \neg q(x)$
\item \pause $\forall x \, .\, p(x) \imp \neg q(x)$
\item \pause $\exists x \, . \, (p(x) \land  \neg q(x)) \lor (\neg
p(x) \land q(x))$
\item \pause
$\forall x\, .\, (\exists y \,.\,
  q(x,y) \land \neg p(x,y) \land \neg r(x,y))$ 
\end{enumerate}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Exercice 6.18, partie II.3 du chapitre 6}
Dans le langage de signature fonctionnelle $\{a^0, f^2\}$ et de
signature relationnelle $\{R^2, S^1\}$, on considère les termes $t_i$
et les formules $\varphi_j$ suivants.
\begin{itemize}
\item $t_1 = f(x,y)$
\item $t_2 = f(a,y)$
\item $t_3 = a$
\item $t_4 = f(x,f(x,x))$
\item $\varphi_1 : R(x,y) \imp \forall y \,. \, S(y)$
\item $\varphi_2 : 
  (\forall y \, .\, R(y,a) ) \imp 
  (\exists y \, .\, R(x,y))$
\item $\varphi_3 : 
  (\forall x \,.\,  \exists z \,.\, R(x,z))
  \land 
  (\exists x \,.\,  \forall y \,.\, R(y,x))$
\end{itemize}
Déterminer si $t_i$ est substituable à $x$ dans $\varphi_j$ et
calculer,  le cas échéant, $\varphi_j (t_i/x)$ pour tout $i$ et $j$
entre 1 et 4. Dans le cas où le terme $t_i$ n'est pas substituable,
renommer les variables de la formule afin qu'il le soit.
\end{frame}

\begin{frame}
\frametitle{Sémantique du calcul des prédicats}
\framesubtitle{Exercice 6.19, partie II.3 du chapitre 6}
Dans un langage de signature relationnelle $\{R^2, =^2\}$,
on considère les formules suivantes:
\begin{eqnarray*}
 \Gamma_1 &=&\forall x \,.\, \exists y\, .\, R(x,y) \\
 \Gamma_2 &=&\forall x \,.\, (\forall y\, .\, 
 (\exists z \, .\, R(x,z) \land R(z,y)) \imp R(x,y)) \\
 \Gamma_3 &=&\forall x,y \,.\, (R(x,y) \land R(y,x))
 \eqv y=x \\
 \Gamma_4 &=&\forall x,y \,.\, 
 (\exists z \, .\, \neg R(z,x) \land \neg R(z,y)) \lor x =y
\end{eqnarray*}
Déterminer la valeur de vérité de ces formules dans les
interprétations suivantes :
\begin{itemize}
\item $\mathcal{U}_1= \N$ et 
$R(x,y)$ est vraie si et seulement si  $x\le y$. 
Le prédicat $=$ a l'interprétation standard.

\item $\mathcal{U}_2= \N\setminus \{0\}$ et 
$R(x,y)$ est vraie si et seulement si  $x \neq y$ et $x$ divise $y$. 
Le prédicat $=$ a l'interprétation standard.
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Mise en forme prénexe}
Mettre sous forme prénexe les formules suivantes
(exemple 6.20, partie III.1.1.)

\begin{tabular}{c l} $F_1$ & $\forall
y\, .\, ({\rm cr}(y)\imp\exists x\, .\,  {\rm co}(x,y))$ \\ 
$F_2$ & $\forall x, y  \, .\, ({\rm cr}(y)\et {\rm co}(x,y)) \imp {\rm
  mal}(x)$ \\ 
$F_3$ & $\forall x\, .\, {\rm ar}(x)\imp {\rm mal}(x)$ \\
$F_4$ & $\forall x\, .\, ({\rm mal}(x) \et {\rm ar}(x)) \imp
(\forall y\, .\,  {\rm cr}(y) \imp \neg {\rm co}(x,y))$ \\ 
$F_5$ & $\exists x \, .\, {\rm cr}(x)$ \\
$F_6$ & $\non (\exists x \, .\,{\rm mal}(x) \et \non {\rm ar}(x))$ \\
\end{tabular}
\pause

\begin{tabular}{c l}
$F_1$ & $\forall y\,.\,\exists x \, .\, (\non{\rm cr}(y)\ou{\rm co}(x,y))$ \\
\pause $F_2$ & $\forall x, y \, .\, (\non{\rm cr}(y)\ou\non{\rm
co}(x,y)\ou{\rm mal}(x))$ \\
\pause $F'_3$ & $\forall x \, .\, (\non{\rm ar}(x)\ou{\rm mal}(x))$ \\
\pause $F_4$ & $\forall x,y \, .\, (\non{\rm mal}(x)\ou\non
{\rm ar}(x)\ou\non{\rm cr}(y)\ou\non{\rm co}(x,y))$ \\
\pause $F_5$ & $\exists x\,.\, {\rm cr}(x)$ \\
\pause $F_6$ & $\forall x\,.\, (\non{\rm mal}(x)\ou{\rm ar}(x))$ \\
\end{tabular}

\end{frame}


\begin{frame}
\frametitle{Calcul des prédicats}
\framesubtitle{Skolémisation}
Skolémiser les formules sous forme prénexe obtenues dans l'exercice
précédent
\end{frame}

% 
% \begin{frame}
% \frametitle{Calcul des prédicats}
% \framesubtitle{Exercice 2}
% \begin{itemize}
%   \item Une formule est close si toutes ses variables sont liées
% \end{itemize}
% \end{frame}