Cette introduction a pour but de rappeler les bases de la logique qui
sous-tend les mécanismes fondamentaux de l'Intelligence Artificielle, comme
déduction, abduction, etc\ldots.\\


\subsubsection{Calcul des propositions}

Une {\it{proposition}} est un énoncé déclaratif (ou assertion) possédant par
définition une seule {\it{valeur de vérité}} : $V$(vraie) ou $F$(fausse).\\
En langage naturel une proposition est en général une affirmation comme :
\begin{itemize}
\item la pluie mouille,
\item il pleut,
\item je suis dehors,
\item je suis mouillé.
\end{itemize}

Ces affirmations sont des éléments d'information atomiques.\\

Les propositions sont représentées symboliquement par les éléments d'un
ensemble dénombrable (un {\it{alphabet}}) appelés {\it{littéraux}}.\\

Une application $val$ (valeur de vérité) de l'ensemble des propositions
$\left\{ X \right\}$ est définie sur l'ensemble $\left\{0,1\right\}$ :
\begin{eqnarray}
\left\{X\right\}\stackrel{val}{\longrightarrow}\left\{0,1\right\}\\
val(p)\longrightarrow\left\{{\begin{array}{c}{0}\\{1}\end{array}}\right\}\nonumber
\end{eqnarray}


\paragraph {Foncteurs de vérité unaires}
Il s'agit d'applications de l'ensemble $\left\{ X \right\}$ des propositions
possibles sur lui-m\^eme.
\begin{eqnarray}
  \left\{X\right\}\stackrel{f}{\longrightarrow}\left\{X\right\}\\
  f(p)\longrightarrow q \nonumber
\end{eqnarray}

A chacune de ces applications $f$ correspond une application de
$\left\{0,1\right\}$ sur lui-m\^eme :
\begin{equation}
 \begin{array}{ccc}
p & \stackrel{f}{\longrightarrow} & q \\
\Bigg\downarrow va l& & \Bigg\downarrow val \\
\left\{0,1\right\} & \stackrel{\varphi}{\longrightarrow} & \left\{0,1\right\}
 \end{array}
\end{equation}
On a donc :\\
\begin{equation}
val\left( f \left( p \right) \right) = \varphi \left( val \left( p \right) \right)
\end{equation}

Dans le cas de la logique bivalente 4 foncteurs unaires $f$ sont possibles :\\

\vspace{0.5cm}
\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{2cm}|p{2cm}|p{2cm}|p{2cm}|p{2cm}|p{2cm}|}
% LIGNE 1
\hline
$p$ &$val(p)$&$f_1(p)$&$f_2(p)$&$f_3(p)$&$f_4(p)$ \\
%       LIGNE 2
\hline
$V$ &$1$&$1$&$1$&$0$&$0$\\
%       LIGNE 3
\hline
$F$ &$0$&$1$&$0$&$1$&$0$\\
\hline
\end{tabular}\\
\caption{Table des foncteurs unaires en logique bivalente}
\label{foncteurs}
\end{figure} 
Dans le reste du texte, la relation d'équivalence $\equiv$ sera remplacée par sa
version ``opérationnelle'' $\leftrightarrow$.\\
Les foncteurs $f_1$ et $f_4$ sont les constantes $1$ et $0$ respectivement.
Le foncteur $f_3$ est appelé {\it{négation de $p$}}, il est dénoté par $\neg
p$. $f_2$ est la {\it{négation}} de $f_3$ qui possède la m\^eme table de
vérité que $val$. Cette double négation définit la loi d'{\bf{idempotence}} :
\begin{equation}
\neg \left( \neg p \right) \equiv p
\end{equation}


\paragraph {Foncteurs de vérité binaires (interpropositionnels)}

Il s'agit d'applications $f$ de l'ensemble produit $X \times X$ dans $X$, avec
$X$ l'ensemble des propositions possibles.

\begin{eqnarray}
X \times X \stackrel {f}{\longrightarrow} X\\
f(p,q) = r
\end{eqnarray}

Un tableau similaire à celui présenté en figure~\ref{foncteurs} peut \^etre
établi à partir du diagramme suivant :

\begin{equation}
 \begin{array}{ccc}
p \times q & \stackrel{f}{\longrightarrow} & r \\
 val \times val\Bigg\downarrow& & \Bigg\downarrow val \\
\left\{0,1\right\}\times \left\{0,1\right\} & \stackrel{\varphi}{\longrightarrow} & \left\{0,1\right\}
 \end{array}
\end{equation}

avec :

\begin{equation}
val \left( f \left( p , q \right) \right) =
        \varphi \left( val \left( p \right) , val \left( q \right) \right)
\end{equation}

Ce tableau (figure~\ref{fonctbinaires}) met en évidence les 16
foncteurs de vérité binaire. Un sémantique classique est précisée pour
chacun des foncteurs.
\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{0.75cm}|p{0.75cm}|p{0.75cm}|p{0.75cm}|p{0.75cm}|p{2cm}|p{4cm}|}
% LIGNE 1
\hline
&&&&&notation&sémantique \\
\hline
$p$ &1&1&0&0&& \\
\hline
$q$ &1&0&1&0&&  \\
\hline
\hline
1&1&1&1&1&&tautologie\\
\hline
2&1&1&1&0&$\vee$&ou inclusif\\
\hline
3&1&1&0&1&$\Leftarrow$&$p$ si $q$ \\
\hline
4&1&1&0&0&&$f_4(p.q) = p$\\
\hline
5&1&0&1&1&$\Rightarrow$&$p$ implique $q$\\
\hline
6&1&0&1&0&&$f_6(p.q) = q$\\
\hline
7&1&0&0&1&$\Leftrightarrow$&$p$ si et seulement si $q$\\
\hline
8&1&0&0&0&$\wedge$&$p$ et $q$ \\
\hline
9&0&1&1&1&$\mid$&NAND incompatibilité \\
\hline
10&0&1&1&0&$\oplus$&XOR alternative, ou exclusif \\
\hline
11&0&1&0&1&& \\
\hline
12&0&1&0&0&& \\
\hline
13&0&0&1&1&& \\
\hline
14&0&0&1&0&& \\
\hline
15&0&0&0&1&$\downarrow$&NOR - rejet \\
\hline
16&0&0&0&0&&antilogie \\
\hline
\end{tabular}
\caption{Table de vérité (foncteurs binaires) $f(p,q)=r$}
\label{fonctbinaires}
\end{figure}

Les notations sont indicatives et varient selon les auteurs.\\
La sémantique indiquée doit \^etre considérée avec précaution. Le sens usuel
des termes ``implique'', tautologie, antilogie, etc. sont souvent différents
de la stricte interprétation en logique. Ainsi la proposition $\left[ p \Rightarrow q
\right]$ est toujours vraie sauf si $p=1$ et $q=0$, ce qui signifie seulement
que le vrai ($1$) ne peut impliquer le faux ($1$).


\paragraph {Expressions Bien Formées (EBF)}

Les foncteurs binaires permettent de transformer des propositions simples en
propositions complexes que l'on appelle le plus souvent des formules. Une
formule sera libéllée en majuscules. Toutes les formules possibles (combinant
des littéraux de propositions simples, des opérateurs, des connecteurs, des
parenthèses) ne sont pas forcément bien formées pour constituer à leur tour
une expression trouvant sa valeur dans le système formel.
Quatre règles doivent \^etre respectées pour qu'une formule soit bien formée :
{\it{
\begin{itemize}
\item règle 1 : un littéral de proposition simple est une EBF de m\^eme que
  les constantes logiques V (vrai) et F (faux),
\item règle 2 : $P$ étant une formule, si $P$ est une EBF alors $\neg P$ est
  une EBF,
\item règle 3 : $P$ et $Q$ étant deux formules, si $P$ et $Q$ sont des EBF
  alors $P \Rightarrow Q$ est une EBF.
\item règle 4 : rien n'est une EBF sinon les suites de symboles produites aux
  règles 1 à 3 précédentes.
\end{itemize}
}}
Ces règles permettent de distinguer :
\begin{itemize}
\item la fausseté d'une formule qui caractérise un énoncé ayant pour valeur de
 vérité F,
\item l'absence de signification qui caractérise un énoncé dénué de sens,
\end{itemize}
Par exemple, $\left[ \neg \left( \Rightarrow pq \right) \right] $ n'est pas un
    énoncé faux mais un énoncé dénué de sens (n'est pas une EBF).


\paragraph {Calcul des propositions : évaluation des EBF}

Le calcul des propositions consiste à trouver la valeur de vérité d'une
formule $P$ composée de propositions atomiques $p_1 \ldots p_i \ldots p_n$.\\

Deux méthodes sont disponibles :
\begin{itemize}
\item la méthode des tables de vérité,
\item la méthode de parcours d'arbre de solutions.
\end{itemize}

Si on considère qu'une tautologie est une formule dont les valeurs de vérité
sont toutes vraies, alors une tautologie peut s'appeler une formule valide (on
dit aussi qu'une formule valide constitue une loi logique).\\

La logique {\it{formelle}} peut alors \^etre considérée comme la recherche de
toutes les tautologies possibles.

Le chap\^{\i}tre suivant présente un certain nombre de lois logiques
constituant la base de la logique formelle.\\


\paragraph {Principales lois logiques (tautologies)}


\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{3cm}|p{8cm}|}
\hline
$p \Leftrightarrow p$&loi d'identité\\
\hline
$p \Rightarrow p$& tautologie élémentaire\\
\hline
$p \Leftrightarrow \left( p \vee p \right)$& lois d'idempotence\\
$p \Leftrightarrow \left( p \wedge p \right)$& des connecteurs $\vee$ et
$\wedge$\\
\hline
$\neg \left( p \wedge \neg p \right) \Leftrightarrow V$ & loi de non
contradiction\\
&deux formules $p$ et $\neg p$ ne peuvent \^etre toutes les deux vraies.\\
\hline
$p \vee \neg p \Leftrightarrow V$& loi du tiers exclu\\
&deux formules $p$ et $\neg p$ ne peuvent toutes les deux fausses.\\
\hline
$\neg \neg p \Leftrightarrow p$&loi de la double négation\\
\hline
\end{tabular}
\caption{Lois élémentaires sur une proposition unique}
\label{loiselem}
\end{figure}

Les lois présentées dans la figure~\ref{loiselem} sont à la base de nombreuses
simplifications. L'absorption est une autre façon de simplifier les
formules. Les différentes lois permettant d'autres simplifications (ou
développements) avec les connecteurs
$\vee$ et $\wedge$ sont présentées dans le
tableau suivant (figure~\ref{absorption}) :\\

\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{6cm}|p{5cm}|}
% LIGNE 1
\hline
$ \left( p \vee q \right) \Leftrightarrow \left( q \vee p \right)$&\\
& Commmutativité\\
$ \left( p \wedge q \right) \Leftrightarrow \left( q \wedge p \right)$ &\\
\hline
$\left( \left( p \vee q \right) \vee r \right) \Leftrightarrow \left(  p \vee \left(
  q \vee r \right) \right)$&\\
&Associativité\\
$\left( \left( p \wedge q \right) \wedge r \right) \Leftrightarrow \left(  p \wedge \left(
  q \wedge r \right) \right)$&\\
\hline
$\left(  p \vee \left( q \wedge r \right) \right) \Leftrightarrow \left( p
  \vee  q \right) \wedge \left( p \vee r \right)$&\\
&Double distributivité\\
$\left(  p \wedge \left( q \vee r \right) \right) \Leftrightarrow \left( p
  \wedge  q \right) \vee \left( p \wedge r \right)$&\\
\hline
$p \wedge \left( p \vee q \right) \Leftrightarrow p$&\\
&Absorption\\
$p \vee \left( p \wedge q \right) \Leftrightarrow p$&\\
\hline
\end{tabular}
\caption{Lois de commutativité, associativité, double distributivité et
  absorption}
\label{absorption}
\end{figure}

Un certain nombre de lois permettent d'établir des dualités d'écriture de
connecteurs en termes d'autres connecteurs. Ces lois sont connues sous le nom
de lois de {\bf DE MORGAN} (tableau de la figure~\ref{morgan}).

\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{5cm}|p{6cm}|}
% LIGNE 1
\hline
$\neg \left( p \wedge q \right) \Leftrightarrow \neg p \vee \neg q$&\\
$\neg \left( p \vee q \right) \Leftrightarrow \neg p \wedge \neg q$&\\
$ \left( p \Rightarrow q \right) \Leftrightarrow \left( \neg p \vee q \right)$&\\
$(p \Rightarrow q) \Leftrightarrow \neg \left( p \vee \neg q \right)$&Lois de dualité ou lois DE MORGAN\\
$\left( p \Leftrightarrow q \right) \Leftrightarrow \left( p \Rightarrow q \right) \wedge \left( q \Rightarrow p \right)$&\\
$\left(p \vee q \right) \Leftrightarrow \left( \neg p \Rightarrow q \right)$&\\
$\left(p \wedge q \right) \Leftrightarrow \neg \left( p \Rightarrow \neg q \right)$&\\
\hline
\end{tabular}
\caption{Lois de DE MORGAN}
\label{morgan}
\end{figure}

Le tableau suivant (figure~\ref{implication}) présente quelques lois dites de
l'implication.\\

\begin{figure}[h]
%     TABLEAU
%
\begin{tabular}{|p{5cm}|p{6cm}|}
% LIGNE 1
\hline
$\left( p \Rightarrow q \right) \Leftrightarrow \left( \neg q  \Rightarrow \neg p \right)$&Loi de
contraposition\\
\hline
$\left( \left( p \Rightarrow q \right) \wedge \left( q \Rightarrow r \right)
\right) \Rightarrow \left( p \Rightarrow r \right)$&Loi de la transitivité et
de l'implication\\
\hline
$\left( \left( p \Rightarrow q \right) \wedge \left( p \Rightarrow \neg q
  \right) \right) \Rightarrow \neg p$&Loi de réduction à l'absurde\\
\hline
$\left( \neg p \Rightarrow p \right) \Rightarrow p$&Loi de Clavius\\
\hline
$\left( p \Rightarrow \left( q \Rightarrow p \right)\right) \Rightarrow p$&Loi de Pierce\\
\hline
$p \Rightarrow \left(q \Rightarrow p\right)$&{\it Verum sequitur ad quodlibet},
une proposition vraie est impliquée par n'importe quelle autre proposition.\\
\hline
$\neg p \Rightarrow \left( p \Rightarrow q \right)$&Ex falso sequitur
quodlibet (à partir du faux on peut déduire n'importe quoi)\\
\hline
$\left( \left( p \Rightarrow q \right) \wedge p \right) \Rightarrow q$&Modus
ponens {\it (latin pono : poser ou affirmer)}\\
\hline
$\left( \left( p \Rightarrow \neg q \right) \wedge q \right) \Rightarrow \neg
p$&Modus tollens {\it(latin tollo : enlever ou nier)}\\
\hline
$\left( p \Rightarrow \left( q \Rightarrow r \right)\right) \Leftrightarrow
\left( \left( p \wedge q \right) \Rightarrow r \right)$& Principe ``{\it
  d'import-export}''\\
\hline
\end{tabular}
\caption{Lois d'implication}
\label{implication}
\end{figure}
 

\paragraph {Substitution et remplacement}

L'opérateur de substitution permet de formaliser la propagation d'une formule
par le remplacement d'un littéral partout où il apparait dans une autre
formule.\\
L'expression de la substitution s'écrit :\\
\begin{tabular}[h]{|p{5cm}|p{6cm}|}
\hline
\begin{equation}
S \left( Q , p, P \right)
\end{equation}
&\vspace{0.4cm}
Substitution de $Q$ à $p$ dans $P$\\
\hline
\end{tabular}\\
\vspace{0.5cm}

Par exemple :\\
\begin{equation}
\begin{array}{l}
P : p \Rightarrow \left( q \Rightarrow p \right)  \\
Q : p \Rightarrow q  \\
S \left( Q , q, P \right)=\mbox{ Substituer }Q 
\mbox{ à toutes les occurences de }q \mbox{ dans }  P  \\
\mbox{On obtient }p \Rightarrow \left(\left( p \Rightarrow q \right)
  \Rightarrow p \right)
\end{array} 
\end{equation}

\newtheorem{theorem}{Théorème}[section]
\begin{theorem}
Si $P$ est une tautologie et $Q$ une EBF alors $S \left( Q , q, P \right)$ est
une tautologie.
\end{theorem}
\newtheorem{corollary}{Corollaire du théorème}[section]
\begin{corollary}
Si $R$ est une tautologie et $P$ une formule constituante de $R$ et si $\left(
  P \Rightarrow Q \right)$ est une tautologie, alors l'expression obtenue en
remplaçant $P$ par $Q$ dans une ou plusieurs occurences quelconques de $P$
dans $R$ est une tautologie.
\end{corollary}


\paragraph {La règle d'élimination}

C'est une tautologie permettant de simplifier grand nombre de formules. Cette
règle (que le lecteur démontrera facilement) indique :
\begin{equation}
\left( P \vee Q \right) \wedge \left( \neg P \vee R \right) \Rightarrow Q \vee
R \hspace{3cm}\left( P \mbox{ est ``dissous''!}\right)
\end{equation}

\paragraph {Jeu de connecteurs fonctionnellement complet}
Les 16 connecteurs de la table de vérité décrite en figure~\ref{fonctbinaires}
peuvent \^etre tous représentés à l'aide des seuls connecteurs :
\begin{itemize}
\item conjonction $\vee$
\item disjonction $\wedge$
\item implication $\Rightarrow$
\end{itemize}

Ainsi, $p \Rightarrow q$ équivaut à $\neg \vee q$.\\
On appelle fonctionnellement complet le jeu de connecteurs qui permet
d'obtenir tous les autres par définition.\\
En conséquence toute EBF peut \^etre ramenée à une formule où ne figurent que
les opérateurs $\neg$, $\wedge$, $\vee$, formant le concept des {\it formes normales
  d'une EBF}.


\paragraph {Formes normales d'une EBF}
\newtheorem{definition}{Définition}[section]
\begin{definition}
On appelle forme normale disjonctive distinguée (FNDD) d'une expression $P$ une
forme disjonctive équivalente à $P$ (m\^emes valeurs de vérité) et dont tous les
membres disjonctifs contiennent {\bf une et une seule fois chacun} des littéraux
propositionnels figurant dans $P$.
\end{definition}
Pour écrire la FNDD d'une expression donnée, il suffira d'énumérer chacun des
cas où l'expression prend la valeur $V$ (vraie).\\


\begin{definition}
On appelle forme normale conjonctive distinguée (FNCD) d'une expression $P$
une forme conjonctive équivalente à $P$ dont tous les facteurs contiennent une
et une seule fois chacun des littéraux propositionnels figurant dans $P$, ces
littéraux étant ou non affectés de négation.
\end{definition}

Pour écrire la FNCD d'une expression, il suffira d'inventorier chacun des cas
où l'expression P prend la valeur $F$ (faux).\\

On notera qu'une FNCD est une conjonction de disjonctions élémentaires.\\
{\bf Remarque} : Les disjonctions citées dans la définition sont appellées
{\bf clauses} et la FNCD est une {\bf forme clausale}.\\

Ces définitions servent à la résolution de calcul de propositions pour la
démonstration automatique de tautologies.


\paragraph {Forme clausale de KOWALSKI}

La forme clausale de Kowalski est une forme abrégée de la notation clausale
précédente :
\begin{equation}
P_1, P_2, \ldots, P_m \Leftarrow Q_1, Q_2, \ldots, Q_n
\end{equation}
Les virgules à {\bf gauche} sont à lire {\bf ou},\\
Les virgules à {\bf droite} sont à lire {\bf et},\\
La fl\^eche orientée à gauche se lit {\bf si},\\
Les $P_i$ et $Q_j$ sont appelés {\bf clauses},\\
Les clauses $P_i$ sont appelées {\bf conclusions},\\
Les clauses $Q_i$ sont appelées {\bf conditions}.\\
La forme généralisée introduit les valeurs $F$ (faux) et $V$ :
\begin{equation}
P_1, P_2, \ldots, P_m,F \Leftarrow Q_1, Q_2, \ldots, Q_n,V
\end{equation}

Plusieurs cas particuliers sont distingués :
\[
\begin{array}{|l|l|}
\hline
m > 1 &\mbox{les conclusions sont multiples, c'est le cas non déterministe.}\\
\hline
m \le 1 &\mbox{Cas particulier des clauses dites {\bf clauses de HORN}}\\& \mbox{du nom
  d'un chercheur américain (1951)}\\
\hline
m = 1 & P \Leftarrow Q_1, Q_2, \ldots, Q_n\\
n > 0 & \mbox{clauses définies. Il existe une conclusion.}\\& \mbox{C'est le cas
  déterministe.}\\
\hline
m = 1 &P \Leftarrow V\\
n = 0 &\mbox{clause définie inconditionnelle : c'est un {\bf fait}}\\&\mbox{ ou une {\bf
  assertion} ou encore un {\bf axiome}.}\\
\hline
m = 0 &F \Leftarrow Q_1, Q_2, \ldots, Q_n\\
n > 0 & \mbox{négation formelle de la conjonction des }Q_j  \\
\hline
m =0 & F \Leftarrow V\\
n=0 & \mbox{une antilogie fondamentale}\\
\hline
\end{array}
\]

\paragraph {La preuve par l'absurde ou réfutation}
Prouver qu'une clause est vraie revient à prouver que la négation de cette
clause est une contradiction (antilogie).

Ce type de preuve est bien traité dans le cas des clauses de HORN\@. La
résolution est basée sur trois {\it{schémas }}\/appliqués de manière
systèmatique.


\paragraph{Schéma 1}

\[
\begin{array}{ll}
P \Leftarrow Q,R&P \mbox{ si } Q \mbox{ et } R\\
&\mbox{ et }\\
F \Leftarrow P&P \mbox{ est } faux\\
&\mbox{ alors}\\
\cline{1-1}
F \Leftarrow Q,R&\left( Q \mbox{ et } R \right) \mbox{ est faux, c'est à dire
  non vrais en m\^eme temps}
\end{array}
\]

\paragraph{Schéma 2}

\[
\begin{array}{ll}
P \Leftarrow V&P \mbox{ est vrai}\\
&\mbox{ et }\\
F \Leftarrow P,Q&\left( P \mbox{ et } Q \right)\mbox{ est faux (pas vrais en
m\^eme temps)}\\
&\mbox{ alors}\\
\cline{1-1}
F \Leftarrow Q& Q \mbox{ est faux}
\end{array}
\]

\paragraph{Schéma 3}

\[
\begin{array}{ll}
P \Leftarrow V&P \mbox{ est vrai}\\
&\mbox{ et }\\
F \Leftarrow P&P \mbox{ est faux}\\
&\mbox{ alors}\\
\cline{1-1}
F \Leftarrow V& \mbox{\bf contradiction}
\end{array}
\]

\paragraph{Schéma 4}

En généralisant :
\[
\begin{array}{lcl}
P_1 \Leftarrow Q_1, Q_2, \ldots, Q_n&&\\
F \Leftarrow P_1, P_2, \ldots, P_m&&\\
&&\mbox{alors}\\
\cline{1-1}
F \Leftarrow Q_1, Q_2, \ldots, Q_n,P_1, P_2, \ldots, P_m&&
\end{array}
\]
Les calculs ainsi présentés font appara\^{\i}tre les clauses opérandes au
dessus de la ligne de points, et la clause résultante en dessous d'elle.\\

Le processus de démonstration est rarement linéaire. Les schémas sont
appliqués dans l'ordre aux clauses. Les clauses résultantes sont ajoutées à la
base de connaissances. En cas d'impasse (plus de schéma applicable), un retour
en arrière est fait (backtracking), pour recommencer l'application des schémas
aux autres clauses.



\subsubsection{Calcul des prédicats}
\label{sec:predicats}

Le calcul des prédicats est une extension du calcul des propositions. Appelé
également logique du premier ordre (LPO), ou logique des prédicats, il est à
la base des langages de programmation logique comme PROLOG par exemple. La puissance
d'expression du calcul des prédicats repose sur l'apparition des
{\bf{variables, quantificateurs et fonctions}}.


\paragraph {Termes}

Les constantes, les variables et les fonctions sont appelées {\bf{termes}}.
\begin{itemize}
\item une constante est un sous-ensemble des symboles autorisés du
  domaine, comme -Jean, 23.56, V2, \ldots-\footnote{Les constantes
    ``caractères'' sont le plus souvent représentées par des
    cha\^{\i}nes de caractères commençant par une lettre majuscule.},
\item une variable est un sous-ensemble de symboles autorisés du domaine qui
  prend des constantes comme valeurs\footnote{Les noms de variables commencent
    le plus souvent par une lettre minuscule.},
\item une fonction est une applicatin de l'ensemble des constantes dans
  lui-m\^eme, comme - Nom(Jean), SquareRoot(16), \ldots-
\end{itemize}


\paragraph {Les prédicats}

Un prédicat est l'application de l'ensemble des constantes dans l'ensemble
(VRAI, FAUX)\footnote{En langue naturelle, un prédicat est le plus souvent
  exprimé par un verbe.}. Par exemple,$EST\_DANS(Boite,y)$, est un prédicat à
deux variables. La première est instanciée par Boite, tandis que la seconde
est libre. Une variable peut \^etre instanciée par une liste de constantes.
Les formules atomiques sont des combinaisons de prédicats avec leurs
arguments. Les littéraux sont à la fois les formules atomiques et leur
négation.


\paragraph {Quantificateurs}

Les quantificateurs sont ceux habituellement utilisés en mathématiques :
\begin{itemize}
\item $\exists{}$ comme dans $[\exists x, OISEAU(x) \cap VERT(x)]$
\item $\forall{}$ comme dans $[\forall x, OISEAU(x) \rightarrow PLUME(x)]$
\end{itemize}
\begin{center}
L'ordre des quantifieurs est très important pour l'évaluation d'une
expression. Par exemple :
\begin{equation}
[\forall{x},\exists{y},CONNAIT(x,y)]
\end{equation}
qui signifie : `` Toute (personne) x connait au moins une autre (personne)
y'', très différent de~:
\begin{equation}
[\exists{x},\forall{y},CONNAIT(x,y)]
\end{equation}
qui signifie~: `` Il existe une (personne) x qui connait toutes les
(personnes) y''.
\end{center}
Les variables utilisées avec un quantificateur sont dites {\bf{liées}} et les
autres sont {\bf{libres}}.

\paragraph {Formules bien formées}

Les formules bien formées\footnote{Well-formed formula en anglais.} sont
définies récursivement. Les littéraux sont des formules bien formées.

\paragraph {Notion de clause}
La démonstration de théorème utilise des expressions logiques mises sous forme
clausale (sous forme de clauses). Une clause est une formule bien formée
consistant en des disjonctions de littéraux. Un algorithme a été proposé par
Winston pour construire des clauses à partir de formules logiques~:
\begin{enumerate}
\item Eliminer les implications
\item Déplacer les négations dans les formules atomiques
\item Eliminer les quantificateurs existentiels
\item Renommer les variables si nécessaire
\item Déplacer les quantificateurs universels vers la gauche
\item Déplacer les disjonctions dans les littéraux
\item Eliminer les conjonctions
\item Renommer les variables, si nécessaire
\item Eliminer les quantificateurs universels
\end{enumerate}

Reprenons un exemple souvent cité dans les ouvrages~:

{\it{Etre un terrien implique trois choses~:
\begin{enumerate}
\item le terrien vit sur la Terre
\item il n'existe pas de Martien qui soit parent avec un Terrien
\item il n'existe pas de non Terrien qui soit connu d'un Terrien

\end{enumerate}}
}
On peut reformuler cet énoncé de la manière suivant en formules logiques~:
\begin{equation}
  \begin{array}{ll}
[\forall x,& TERRIEN(x) \rightarrow [[ \exists y, VIVRE\_SUR(x,y) \cap TERRE(y)]\\
&[\neg \exists y, PARENT(x,y)\cap MARTIEN(y)]\\
&[\forall y,\neg TERRIEN(y) \rightarrow \neg CONNU(x,y)]]]
\end{array}
\end{equation}
\paragraph{Elimination des implications}
\begin{equation}
  \begin{array}{ll}
[\forall x,& \neg TERRIEN(x) \cup [[ \exists y, VIVRE\_SUR(x,y) \cap TERRE(y)]\\
&[\neg \exists y, PARENT(x,y)\cap MARTIEN(y)]\\
&[\forall y,TERRIEN(y) \cup \neg CONNU(x,y)]]]
\end{array}
\end{equation}
\paragraph{Déplacer les négations dans les formules atomiques}
\begin{equation}
  \begin{array}{ll}
[\forall x,& \neg TERRIEN(x) \cup [[ \exists y, VIVRE\_SUR(x,y) \cap TERRE(y)]\\
&[\forall y,\neg PARENT(x,y)\cup \neg MARTIEN(y)]\\
&[\forall y,TERRIEN(y) \cup \neg CONNU(x,y)]]]
\end{array}
\end{equation} 
\paragraph{Elimination des quantificateurs existentiels}
Dans cette phase, les fonctions dites de {\bf{skolem}} doivent \^etre
introduites. Une fonction de skolem sert à substituer une variable quantifiée
existentiellement. Elle s'exprime en fonction de variables définies par les
quantificateurs universels de l'expression dans laquelle la substitution doit
\^etre faite. Ici, la fonction skolem de la variable existentielle y sera
notée PLANETE(x), soit~:
\begin{equation}
  \begin{array}{ll}[\forall x,& \neg TERRIEN(x) \cup [[ \exists y,
    VIVRE\_SUR(x,PLANETE(x) \cap TERRE( PLANETE(x))]\\
&[\forall y,\neg PARENT(x,y)\cup \neg MARTIEN(y)]\\
&[\forall y,TERRIEN(y) \cup \neg CONNU(x,y)]]]
\end{array}
\end{equation}
\paragraph{Renommer les variables, si nécessaire}
\begin{equation}
  \begin{array}{ll}[\forall x,& \neg TERRIEN(x) \\
& \cup [[VIVRE\_SUR(x,PLANETE(x) \cap TERRE( PLANETE(x))]\\
&[\forall y,\neg PARENT(x,y)\cup \neg MARTIEN(y)]\\
&[\forall z,TERRIEN(z) \cup \neg CONNU(x,z)]]]
\end{array}
\end{equation}
\paragraph{Déplacer les quantificateurs universels vers la gauche}
\begin{equation}
  \begin{array}{ll}
[\forall x,\forall y,\forall z,& \neg TERRIEN(x)\\
&\cup [[VIVRE\_SUR(x,PLANETE(x) \cap TERRE( PLANETE(x))]\\
&[\neg PARENT(x,y)\cup \neg MARTIEN(y)]\\
&[TERRIEN(z) \cup \neg CONNU(x,z)]]]
\end{array}
\end{equation}
\paragraph{Déplacer les disjonctions dans les littéraux}
\begin{equation}
  \begin{array}{ll}
[\forall x,\forall y,\forall z\\
& [\neg TERRIEN(x) \cup VIVRE\_SUR(x,PLANETE(x))]\\
& \cap[\neg TERRIEN(x) \cup TERRE( PLANETE(x))]\\
& [\neg TERRIEN(x) \cup \neg PARENT(x,y) \cup \neg MARTIEN(y)]\\
& [\neg TERRIEN(x) \cup TERRIEN(z) \cup \neg CONNU(x,z)]]
\end{array}
\end{equation}
\paragraph{Eliminer les conjonctions}
\begin{equation}
  \begin{array}{ll}
& [\forall x, \neg TERRIEN(x) \cup [VIVRE\_SUR(x,PLANETE(x)]\\
& [\forall x, \neg TERRIEN(x) \cup TERRE( PLANETE(x))]\\
& [\forall x, \forall y, \neg TERRIEN(x) \cup \neg PARENT(x,y) \cup \neg MARTIEN(y)]\\
& [\forall x, \forall z, \neg TERRIEN(x) \cup TERRIEN(z) \cup \neg CONNU(x,z)]
\end{array}
\end{equation}

\paragraph{Renommer les variables si nécessaire}
\begin{equation}
\begin{array}{ll}
& [\forall x, \neg TERRIEN(x) \cup [VIVRE\_SUR(x,PLANETE(x)]\\
& [\forall u, \neg TERRIEN(u) \cup TERRE( PLANETE(u))]\\
& [\forall v, \forall y, \neg TERRIEN(v) \cup \neg PARENT(v,y) \cup \neg MARTIEN(y)]\\
& [\forall w, \forall z, \neg TERRIEN(w) \cup TERRIEN(z) \cup \neg CONNU(w,z)]
\end{array}
\end{equation}

\paragraph{Eliminer les quantificateurs universels}
\begin{equation}
\begin{array}{ll}
& \neg TERRIEN(x) \cup [VIVRE\_SUR(x,PLANETE(x)\\
& \neg TERRIEN(u) \cup TERRE( PLANETE(u))\\
& \neg TERRIEN(v) \cup \neg PARENT(v,y) \cup \neg MARTIEN(y)\\
& \neg TERRIEN(w) \cup TERRIEN(z) \cup \neg CONNU(w,z)
\end{array}
\end{equation}

Ceci permet la démonstration de théorème.

\paragraph {Algorithme de résolution}
\begin{enumerate}
\item Nier le théorème à prouver et ajouter le résultat dans la liste des
  axiomes
\item Mettre la liste des axiomes sous la forme de clauses
\item Jusqu'à ce que la liste de clauses soit vide (NIL) soit générée ou qu'il
  n'y ait plus de paires de clauses résolvables, chercher les clauses
  résolvables, les résoudre, et les ajouter à la liste des clauses
\item Si la clause vide est générée, annoncer que le théorème est vrai, s'il
  n'y a pas de clause résolvable, annoncer que le théorème est faux.
\end{enumerate}

\subsubsection{Représentation des connaissances par objets}
Imaginer comment représenter les connaissances est une
gageure. La modélisation de la mémoire humaine a inspiré les psychologues, qui
cherchent à reproduire les fonctions et mécanismes de raisonnement pour les
étudier. Les réseaux sémantiques sont issus de ces travaux et sont devenus
depuis des mécanismes récupérés par la communauté informatique pour exprimer
commodément ce qui ``est su'' en général~: ``le sens commun''.

\paragraph {Graphes et réseaux sémantiques}
Les entités présentes dans un réseau sémantique sont respectivement des
noeuds (représentant des objets) et des arcs (représentant des relations entre
ces objets). Le lecteur s'aperçoit bien maintenant des racines des différentes
méthodes d'analyse et conception ``objet''!

Un graphe représentant un réseau sémantique pourrait \^etre celui de la figure \ref{reseau_semantique}.

\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/poly_rep_con_reseau_semantique.eps}}
}
  \caption{Exemple de réseau sémantique}
  \label{reseau_semantique}
\end{figure}

Les réseaux sémantiques ont été utilisés pour l'explication (ou la
compréhension) de phrases, comme~:

\begin{center}
{\it{Le professeur lit l'exercice}}
\end{center}
Le réseau sémantique correspondant est illustré dans la figure \ref{reseau_predicat}.

 \begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/poly_rep_con_reseau_predicat.eps}}
}
  \caption{Réseau équivalent à la phrase}
  \label{reseau_predicat}
\end{figure}

Cette phrase pourrait aussi s'exprimer sous la forme du prédicat~:

\begin{center}
{\it{[LIRE(PROFESSEUR,EXERCICE)]}}
\end{center}

Plus généralement tout objet pourra \^etre représenté avec ses relations avec
les autres selon une structure de réseau sémantique particulière appelée
structure d'objet.

Un objet est défini par un ensemble de propriétés. Ces propriétés sont
classiquement appelées des attributs. Une classe est un ensemble d'objets qui
partagent des caractères communs.
\begin{figure}[h]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/cours-ia-reseau.eps}}
}
  \caption{Exemple de réseau sémantique}
  \label{reseau}
\end{figure}
L'exemple présenté ci-dessus présente le réseau sémantique correspondant à la
phrase :
{\bf{Martin vend une Nevada pour 50~000~francs}}.

On peut faire une équivalence entre réseau sémantique et calcul de prédicat.

La représentation du réseau présenté en figure \ref{reseau} peut s'exprimer
sous la forme suivante :
\begin{equation}
Vendre(Martin,Nevada,50000f)
\end{equation}
Si on généralise la proposition, on l'exprime sous la forme d'un prédicat :
\begin{equation}
( \exists x, \exists y, \exists z )(Vendre(z,x,y) \& agent(z) \& objet(x) \& valeur(y))
\end{equation}

\begin{figure}[t]
\fbox
{
 \centerline{\epsfig{file=/home/am/dessins/cours-ia-reseau2.eps}}
}
  \caption{Réseau plus générale}
  \label{reseau2}
\end{figure}
