\documentclass[12pt, a4paper]{report}

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

\newcounter{conta}

\begin{document}

\noindent {\it TECC: L\'ogica Aplicada a Computa\c c\~ao}
\hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2003 \\
\noindent Professor: Newton Jos\'{e} Vieira \hfill DCC/ICEx/UFMG \\
\noindent {Trabalho Pr\'{a}tico 2} \hfill Entrega: 12/01/04

\begin{enumerate}
 \item  Unifica\c c\~ao

 Dois literais podem ser unificados se existir uma substitui para ambas as vari\'{a}veis. Após a substitui\c c\~ao,
 os literais resultantes s\~o id\^enticos exceto possivelmente pelo sinal. A substitui\c c\~ao
 troca o mesmo termo em todas as ocorrências de uma variável dada.
 O procedimento de unifica\c c\~ao é a forma de unificar dois literais. O procedimento de unifica\c c\~ao sempre
 obt\'{e}m a substitui\c c\~ao mais geral que pode ser achada, se existir, para as duas express\~oes com objetivo de faz\^e-las
 id\^enticas. Quando se tenta unificar dois literais dados, o fato de ser negativo ou positivo \'{e} ignorado.
 Entretanto, para a maioria da regras de infer\^encia, um par de literais \'{e} considerado somente quando eles s\~ao de
 sinais opostos, ou seja, um positivo e outro negativo.

Por exemplo $$FEMALE(Roberta)$$ $$\neg MALE(x)| \neg FEMALE(x)$$
contem literais que podem ser unificados produzindo $$\neg
MALE(Roberta)$$. O procedimento unificação acha a substituição
para a variável $x$ por Roberta. Os literais unificados são
$$FEMALE(Roberta)  \neg
FEMALE(x).$$

Um ponto sutil na unificação é apresentado no exemplo abaixo:
$$GE(sum(x,sum(y,minus(x))),y)$$ $$GE(sum(x,x),y)|
ACCEPTABLE(pair(x,y))$$

A primeira  cláusula diz que $x +(y-x)$ é maior ou igual a $y$. A
segunda cláusula diz que, se $x + x$ é maior ou igual a $y$, então
o par $x$, $y$ é aceitável. Você pode perceber porque não podemos
unificar os  dois literais no predicado GE?

Os dois literais não podem ser unificados pois não existe
substituição para as variáveis que produzam dois novos e idênticos
(exceto pelo sinal) literais. O fato de a mesma variável x
aparecer em ambas as cláusulas não é relevante, já que um variável
só tem significado na cláusula que aparece. Então  para tentar
unificar dois literais de duas cláusulas você deve renomear as
variáveis antes de tentar compartilhá-las nas duas cláusulas.

O objetivo desse trabalho prático é implementar o procedimento
Unificação utilizando o raciocínio acima explicado. Testes deverão
ser executados com o objetivo de avaliar a corretude do programa.
É necessário a implementação utilizando o programa PROLOG já que o
conceito de Unificação é muito importante e utilizado em tal
linguagem.

\end{enumerate}

\end{document}