\documentclass[12pt,a4paper]{article}

\usepackage[portuguese]{babel}
\usepackage{fullpage}

%=================================================================
\addtolength{\topmargin}{.5cm}
%\addtolength{\textheight}{3cm}
%\addtolength{\evensidemargin}{-2cm}
%\addtolength{\textwidth}{2.5cm}
%=================================================================
\newcounter{conta}
\pagestyle{empty}
\begin{document}

\noindent P\'os-Gradua\c{c}\~ao em Ci\^{e}ncia da Computa\c{c}\~{a}o
 \hfill DCC/ICEx/UFMG \\
{\it Automa\c{c}\~ao de Sistemas de Infer\^encia}
 \hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2008 \\
Professor: Newton Jos\'{e} Vieira \hfill  nvieira@dcc.ufmg.br \\

\noindent {\bf Segundo Trabalho.} \hfill {\bf Data de entrega: 8/12/2008}

\vspace*{5mm}
Implementar um algoritmo de unifica\c{c}\~ao para l\'ogica multisortida em que as categorias
sem\^anticas s\~ao organizadas por meio de uma rede taxon\^omica com as seguintes caracter\'{\i}sticas:
\begin{itemize}
 \item para cada constante $C$ existe uma \'unica categoria sem\^antica $\psi$ tal que $C\Rightarrow \psi$;
 \item para cada par de categorias $\psi_1$ e $\psi_2$, ou n\~ao existe categoria sem\^antica $\varphi$
       tal que $\varphi\stackrel{*}{\Rightarrow}\psi_1$ e $\varphi\stackrel{*}{\Rightarrow}\psi_2$, ou ent\~ao
       existe mas para qualquer outra categoria $\varphi'$, se $\varphi'\stackrel{*}{\Rightarrow}\psi_1$ e
       $\varphi'\stackrel{*}{\Rightarrow}\psi_2$, ent\~ao $\varphi'\stackrel{*}{\Rightarrow}\varphi$.
\end{itemize}
O programa dever\'a aceitar uma rede taxon\^omica como entrada satisfazendo essas res\-tri\c{c}\~oes.
Al\'em disso, dever\'a receber como entrada:
\begin{itemize}
 \item para cada vari\'avel, a categoria associada (que deve ser \'unica);
 \item para cada cada s\'{\i}mbolo predicativo de $n$ argumentos, a $n$-upla de categorias associada; e
 \item para cada cada s\'{\i}mbolo funcional de $n$ argumentos, a $n+1$-upla de categorias associada.
\end{itemize}

O algoritmo de unifica\c{c}\~{a}o \'{e} similar ao j\'{a} visto, com as seguintes modifica\c{c}\~{o}es:
\begin{list}{(\alph{conta})}{\usecounter{conta}}
 \item uma vari\'{a}vel $x\!: \psi_1$ unifica com outra $y\!: \psi_2$ se existe
       $\varphi$ tal que $\varphi \stackrel{*}{\Rightarrow}_R \psi_1$ e
       $\varphi \stackrel{*}{\Rightarrow}_R \psi_2$; neste caso,
       ambas as vari\'{a}veis s\~{a}o substitu\'{\i}das por $v\!: \varphi$, sendo
       $v\!: \varphi$ uma nova vari\'{a}vel;
 \item uma vari\'{a}vel $x\!: \psi$ unifica com uma constante $A\!: \varphi$ se
       $\varphi \stackrel{*}{\Rightarrow}_R \psi$; neste caso, $x\!: \psi$ \'{e}
       substitu\'{\i}da por $A\!: \varphi$;
 \item uma vari\'{a}vel $x\!: \psi$ unifica com uma forma funcional $f(t_1, \ldots,
       t_n)$, sendo $f$ associado \`{a} $n+1$-upla $\langle \omega_1, \ldots,
       \omega_n, \varphi \rangle$, se $x\!: \psi$ n\~{a}o ocorre em $f(t_1, \ldots,
       t_n)$ e $\varphi \stackrel{*}{\Rightarrow}_R \psi$; neste caso, $x\!:
       \psi$ \'{e} substitu\'{\i}da por $f(t_1, \ldots, t_n)$.
\end{list}


Procure testar o algoritmo com um conjunto de duplas de termos e f\'ormulas at\^omicas bem
representativas.

\end{document}