\documentclass[11pt]{article}
\usepackage{alltt}
\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{pifont}
\usepackage[dvips]{graphics}
\usepackage[dvips]{graphicx}

\parindent=0cm
\oddsidemargin 0.2cm
\evensidemargin 0.2 cm


\textheight 22cm
\textwidth 16.0cm
\title{\bf Examen de Logique et de  Prolog  --- ESSI2  \\
{\large(Documents autoris\'es: {\it tous})}}
\author{H\'el\`ene Collavizza et Michel Rueher}
\date{Mai 2001}

\begin{document}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Logique}

\begin{enumerate}

\item  {\bf Formalisation (2.5 points)}

Soit le langage du premier ordre composé de l'ensemble de variables $V=\{x,y\}$, les symboles fonctionnels 0-aires $l$ et $s$,
les symboles de prédicats binaires $a$ et $f$.

Dans ce langage, exprimer les énoncés suivants :

\begin{enumerate}

	\item	Tout le monde aime Laurent
	\item	Quelqu'un aime Laurent et sa femme
	\item  Tous ceux qui aiment Laurent n'aiment pas Stéphane		
	\item   Laurent ne peut aimer la femme d'un autre

\end{enumerate}	

\item  {\bf Validité (3.5 points)}

\begin{enumerate}

	\item Soit la formule $F = (\forall~ x \; p(x,x)) \wedge (\forall~ x \forall~ y \forall~ z \; (p(x,y) \wedge p(y,z) \Rightarrow p(x,z))) \wedge (\exists y \; \forall x \; p(x,y))$.

Donner une interprétation $I_1$ qui est un modèle de $F$ et une interprétaion $I_2$ qui n'est pas un modèle de $F$.

    \item Montrer par résolution que la formule $F= \forall~ x \; (p(x) \vee \neg p(x))$ est universellement valide.

\end{enumerate}	

\item  {\bf Preuve dans tous les modèles (5 points)}

Soit les axiomes :

    A1 : $ \forall~ x~  (( A(x) \wedge~ \neg~ B(x)) \Rightarrow~ \exists~ y~  (C(x,y) \wedge~ D(y))) $

    A2 : $ \exists~ x~  (  E(x) \wedge~ A(x) \wedge~ \forall~ y~  (C(x,y) \Rightarrow E(y))) $

    A3 : $\forall~ x~  ( \neg~ E(x) \vee~ \neg~ B(x))$

    Montrer que $\Phi = \exists~  x~  (E(x) \wedge D(x) ) $ est valide dans tous les modèles de \{A1,A2,A3\}.

    


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Prolog}
\begin{enumerate}

\item {Manipulations élémentaires (2 points)}
	\begin{itemize}
\item Construire (et dessiner !) l'arbre de recherche pour la requête

{\tt retrait\_elt0(X,[a,b,Z]) } 
avec la définition du prédicat {\tt retrait\_elt0/2 } ci-dessous:
\begin{verbatim}
retrait_elt0(J,[J|L],L).
retrait_elt0(J,[K|L],[K|M]):- retrait_elt0(J,L,M).
\end{verbatim}
\item Comparer les performances des prédicats {\tt retrait\_elt0/2 } et
{\tt retrait\_elt1/2 }
\begin{verbatim}
retrait_elt1(E,Ldepart,Lresultat):-
      append(L1,[E|L2],Ldepart),
      append(L1,L2,Lresultat).
append([],L,L).
append([T|L1],L2,[T|L3]):- append(L1,L2,L3).
\end{verbatim}
	\end{itemize}

\item {Canmiss(2 points)}\\
Dans le programme ci-dessous (extrait de {\tt canmiss/1} expliquer le rôle du 
prédicat {\tt enum/3}. Pourquoi est-il incorrect de remplacer {\tt enum/3} par
 {\tt enum1/3}.
\begin{verbatim}
genere_etat_valide([Mc,Cc,Rc],[Mn,Cn,Rn]):-
      select(M,C,Mc,Cc),
      Mo is Mc-M,   Co is Cc -C,  ok(Mo,Co),
      Mn is 3 - Mo, Cn is 3 - Co, ok(Mn,Cn),
      succ(Rc,Rn).
select(M,C,Mc,Cc):-
      enum(M,0,Mc),     enum(C,0,Cc),
      MC is M+C,MC >= 1,MC =< 2.
enum(X,_,X).
enum(X,Y,Z):- Z > Y,Z1 is Z-1, enum(X,Y,Z1).
enum1(X,Y,Z):- X =< Z , Y =< Z.
\end{verbatim}


\item { Petit démonstrateur (4 points)}
\begin{itemize}
\item En vous inspirant du méta-interprète Prolog vu en cours, 
écrire un prédicat {\tt solve/1}  qui a pour argument un ensemble de buts à démontrer. la 
démonstration sera basée sur la résolution et utilisera un ensemble de
clauses de Horn.
On supposera que les clauses et les buts à résoudre sont représentés par des listes.\\
Par exemple, les clauses :\\
$
p(X) \Leftarrow q1(X,1) \wedge \;\; \\
p(X) \Leftarrow q2(X,2)\wedge \;\; \\
p(X) \Leftarrow (q3(X,3)\wedge v3(X,3)) \wedge \;\; \\
q1(a1,1)\wedge \\
... $
pourraient être rreprésentées par un fait {\tt list\_of\_clauses/1}  :
\begin{verbatim}
list_of_clauses([[p(X),[q1(X,1)]],[p(X),[q2(X,2)]],[p(X),[q3(X,3),v3(X,3)]],
[q1(a1,1),vide],...]).
\end{verbatim}


\item	Est ce que la strat\'egie de recherche standard de Prolog garantit la
	correction et la compl\'etude des r\'esultats de ce démonstrateur ?\\
	Pourquoi ?
\end{itemize}

\end{enumerate}

\item {DGC (3 points)}\\
Ecrire la DGC qui analyse et évalue des expressions qui respectent la grammaire 
$a^{n}b^n$ où $a$ est un nombre entier et $n$ un chiffre. 
Pour calculer $a^{n}$ on multipliera $n$ fois $a$ par lui-même.\\
Exemple:
\begin{verbatim}
 expr(Z,"2*3",[ ]) -> Z=6
 expr(Z,"2*2*2*3*3*3",[ ]) -> Z=216
 expr(Z,"2*2*2*3*3*3*3",[ ]) -> no
 expr(Z,"2*2*2*3*3*3*3",X) ->
      X = [42,50,42,51,42,51,42,51,42,51],
      Z = 4 ? ;
      X = [42,51],
      Z = 216 ? ;
\end{verbatim}

\end{enumerate}
\end{document}         



