\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

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

\noindent {\bf\Large Constru\c c\~ao de forma clausal:}

\vspace*{5mm}
\begin{flushleft}
{\bf Entrada:} f\'ormula fechada $A$. \\
{\bf Sa\'{\i}da:} $A'$, na forma clausal, tal que $A\approx A'$.
\end{flushleft}

%\vspace*{2mm}
\begin{tabbing}
xx\=xxx\=xxx\= \kill
1. \> Renomeie vari\a'aveis de forma que nenhuma apare\c ca em dois \\
   \> quantificadores. \\
2. \> Elimine todo conectivo bin\a'ario que n\~ao seja $\wedge$ ou $\vee$. \\
3. \> Empurre cada $\neg$ para dentro at\a'e encostar em f\a'ormula at\^omica. \\
4. \> Empurre os quantificadores para fora, formando um prefixo \\
   \> seguido de matriz. \\
5. \> Transforme a matriz para a FNC. \\
6. \> Para cada $\exists x$: \\
   \> \> sejam $y_1,\dots,y_n$ as vari\a'aveis {\em universalmente\/} quantificadas \\
   \> \> que {\em precedem\/} $\exists x$; \\
   \> \> elimine $\exists x$; \\
   \> \> {\bf se} $n>0$ {\bf ent\~ao} \\
   \> \> \> seja $f$ uma {\em nova fun\c c\~ao\/} de $n$ argumentos; \\
   \> \> \> substitua cada ocorr\^encia de $x$ por $f(y_1,\ldots,y_n)$. \\
   \> \> {\bf sen\~ao} ($n=0$) \\
   \> \> \> seja $a$ uma {\em nova contante\/}; \\
   \> \> \> substitua cada ocorr\^encia de $x$ por $a$. \\
   \> \> {\bf fimse}. \\
\end{tabbing}

\pagebreak

\noindent {\bf\Large Algoritmo de unifica\c c\~ao:}

\vspace*{5mm}
\begin{flushleft}
{\bf Entrada:} conjunto de equa\c c\~oes de termos. \\
{\bf Sa\'{\i}da:} conjunto de equa\c c\~oes de termos na forma {\em resolvida\/}
ou ``n\~ao unific\'avel''.
\end{flushleft}

%\vspace*{2mm}
\begin{tabbing}
xxx\=xx\=xxx\=xxx\= \kill
{\bf repita} enquanto aplic\a'avel: \\
\>1. \> transforme $t=x$, onde $t$ n\~ao \a'e vari\a'avel, em $x=t$; \\
\>2. \> elimine a equa\c c\~ao $x=x$; \\
\>3. \> seja $t'=t''$ uma equa\c c\~ao, onde $t'$ e $t''$ n\~ao s\~ao vari\a'aveis;\\
\>   \> {\bf se} os s\a'{\i}mbolos funcionais de $t'$ e $t''$ s\~ao diferentes
                 {\bf ent\~ao} \\
\>   \> \> retorne ``n\~ao unific\a'avel'' \\
\>   \> {\bf sen\~ao} \\
\>   \> \> sejam $t'=f(t_1',\ldots,t_k')$ e $t''=f(t_1'',\ldots,t_k'')$; \\
\>   \> \> substitua a equa\c c\~ao $t'=t''$ pelas $k$ equa\c c\~oes
                  $t_1'=t_1'',\ldots,t_k'=t_k''$ \\
\>   \> {\bf fimse}; \\
\>4. \> seja $x=t$ uma equa\c c\~ao, onde $x$ tem outra ocorr\^encia no conjunto;\\
\>   \> {\bf se} $x$ ocorre em $t$ {\bf ent\~ao} \\
\>   \> \> retorne ``n\~ao unific\a'avel'' \\
\>   \> {\bf sen\~ao} \\
\>   \> \> substitua as ocorr\^encias de $x$ em outras equa\c c\~oes por $t$ \\
\>   \> {\bf fimse} \\
{\bf fimrepita}; \\
retorne o conjunto obtido. \\
\end{tabbing}

\pagebreak

\noindent {\bf\Large Algoritmo de unifica\c c\~ao de Robinson:}

\vspace*{5mm}
\begin{flushleft}
{\bf Entrada:} dois \'atomos $A$ e $A'$. \\
{\bf Sa\'{\i}da:} um {\em umg\/} para $A$ e $A'$ ou ``n\~ao unific\'avel''.
\end{flushleft}

%\vspace*{2mm}
\begin{tabbing}
xxx\=xx\=x\=xxx \kill
$\mu\leftarrow \varepsilon$; \\
{\bf enquanto} $A\not=A'$ {\bf fa\c ca} \\
 \> seja $\{t,t'\}$ o conjunto de discord\^ancia de $A$ e $A'$; \\
 \> {\bf se} $t$ ou $t'$ \a'e uma vari\a'avel $x$ e o outro um termo $u$ \\
 \> \> tal que $x$ n\~ao ocorre em $u$ {\bf ent\~ao} \\
 \> \> \>$\mu\leftarrow \mu\{x\leftarrow u\}$; \\
 \> \> \>$A  \leftarrow A\{x\leftarrow u\}$; \\
 \> \> \>$B  \leftarrow B\{x\leftarrow u\}$ \\
 \> {\bf sen\~ao} \\
 \> \> \>retorne ``n\~ao unific\a'avel'' \\
 \> {\bf fimse} \\
{\bf fimenquanto}; \\
retorne $\mu$. \\
\end{tabbing}


\end{document}
