\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

\pagestyle{empty}
\begin{document} \large

\noindent {\bf\Large Um fragmento da teoria das palavras:}

\vspace*{5mm}
\begin{enumerate}
 \item $\forall x\, \mbox{\em substr\/}(x,x)$
 \item $\forall x\forall y\forall z\, [(\mbox{\em substr\/}(x,y)\wedge
        \mbox{\em suffix\/}(y,z))\rightarrow\mbox{\em substr\/}(x,z)]$
 \item $\forall x\forall y\, \mbox{\em suffix\/}(x,y.x)$
 \item $\forall x\forall y\forall z\, [(\mbox{\em substr\/}(x,y)\wedge
        \mbox{\em prefix\/}(y,z))\rightarrow\mbox{\em substr\/}(x,z)]$
 \item $\forall x\forall y\, \mbox{\em prefix\/}(x,x.y)$
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Na forma clausal:}

\vspace*{5mm}
\begin{enumerate}
 \item[1.] $\mbox{\em substr\/}(x,x)$
 \item[2.] $\neg\mbox{\em substr\/}(x,y)\vee\neg\mbox{\em suffix\/}(y,z)
        \vee\mbox{\em substr\/}(x,z)$
 \item[3.] $\mbox{\em suffix\/}(x,y.x)$
 \item[4.] $\neg\mbox{\em substr\/}(x,y)\vee\neg\mbox{\em prefix\/}(y,z)
        \vee\mbox{\em substr\/}(x,z)$
 \item[5.] $\mbox{\em prefix\/}(x,x.y)$
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Uma refuta\c c\~ao de}
           $\neg\mbox{\em substr\/}(a.b.c,a.a.b.c.c)$:

\vspace*{5mm}
\begin{tabular}{rll}
 6. & $\neg\mbox{\em substr\/}(a.b.c,a.a.b.c.c)$ & neg. da consulta \\
 7. & $\neg\mbox{\em substr\/}(a.b.c,y_1)\vee\neg\mbox{\em suffix\/}(y_1,a.a.b.c.c)$ & 6,2 \\
 8. & $\neg\mbox{\em substr\/}(a.b.c,a.b.c.c)$ & 7,3 \\
 9. &  $\neg\mbox{\em substr\/}(a.b.c,y_2)\vee\neg\mbox{\em prefix\/}(y_2,a.b.c.c)$ & 8,4 \\
10. &  $\neg\mbox{\em substr\/}(a.b.c,a.b.c)$ & 9,5 \\
11. &  $\Box$ & 10,1
\end{tabular}

\pagebreak
\noindent {\bf\Large SLD-resolution:}

\vspace*{5mm}
\noindent Sejam:
\begin{description}
 \item[P:] conjunto de cl\'ausulas de programa;
 \item[R:] regra de computa\c c\~ao;
 \item[G:] cl\'ausula meta.
\end{description}

\noindent Uma {\em deriva\c c\~ao por SLD-resolution\/} \'e uma sequ\^encia de
passos de resolu\c c\~ao entre cl\'ausulas meta e cl\'ausulas de programa,
levando a uma sequ\^encia de cl\'ausulas meta $G_0,G_1,\ldots$, onde:
\begin{enumerate}
 \item[\ ] $G_0$ \'e $G$; e
 \item[\ ] $G_{i+1}$ \'e obtido de $G_i$:
           \begin{itemize}
            \item selecionando-se um literal $A_i$ de $G_i$ de acordo com $R$;
            \item escolhendo-se uma cl\'ausula $C_i$ de $P$ cuja cabe\c ca
                  unifica com $A_i$ com umg $\theta_i$;
            \item e resolvendo:

                  $G_i=\leftarrow A_1,\ldots,A_{i-1},A_i,A_{i+1},\ldots,A_n$

                  $C_i=A\leftarrow B_1,\ldots,B_k$

                  $A_i\theta_i=A\theta_i$

                  $G_{i+1}=\leftarrow (A_1,\ldots,A_{i-1},B_1,\ldots,B_k,A_{i+1},\ldots,A_n)\theta_i$
           \end{itemize}
\end{enumerate}

\pagebreak
\noindent {\bf\Large Exemplo:}

\vspace*{10mm}
\noindent {\Large Dois procedimentos e um banco de dados:}

\vspace*{5mm}
\begin{tabbing}
 xxxxxxxxx\=xxx\=xxxxxxxxxxxxx\=xxx\= \kill
          \>1. \>$q(x,y) \leftarrow p(x,y)$ \\
          \>2. \>$q(x,y) \leftarrow p(x,z), q(z,y)$ \\
          \> \ \\
          \>3. \>$p(b,a)$   \> 7. \>$p(f,b)$ \\
          \>4. \>$p(c,a)$   \> 8. \>$p(h,g)$ \\
          \>5. \>$p(d,b)$   \> 9. \>$p(i,h)$ \\
          \>6. \>$p(e,b)$   \>10. \>$p(h,j)$
\end{tabbing}

\vspace*{8mm}
\noindent {\Large O mesmo programa em Prolog:}

\vspace*{5mm}
\begin{tabbing}
 xxxxxxx\=xxxxxxxxxxxxxxxxxxxxxxx\= \kill
          \>{\tt ancestor(X,Y) :- parent(X,Y).} \\
          \>{\tt ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).} \\
          \> \ \\
          \>{\tt parent(bob,allen).}       \\
          \>{\tt parent(catherine,allen).} \\
          \>{\tt parent(dave,bob).}        \\
          \>{\tt parent(ellen,bob).}       \\
          \>{\tt parent(fred,bob).}        \\
          \>{\tt parent(harry,george).}    \\
          \>{\tt parent(ida,harry).}       \\
          \>{\tt parent(harry,joe).}
\end{tabbing}

\vspace*{5mm}
\noindent {\Large Uma consulta:}

\vspace*{5mm}
\begin{tabbing}
 xxxxxxx\=xxxxxxxxxxxxxxxxxxxxxxx\= \kill
          \>{\tt :- ancestor(Y,bob), ancestor(bob,Z).}
\end{tabbing}

\vspace*{5mm}
\noindent {\Large Resposta:} {\tt Y = dave, Z = allen.}

\end{document}
