\documentclass[12pt, a4paper]{report}

%\pagestyle{empty}
\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 {\bf Segundo TP} \hfill Entrega: 03/02/04

\vspace*{5mm}
Implemente, em sua linguagem de programa\c c\~ao preferida, um sistema de infer\^encia
para o C\'alculo de Predicados baseado em {\em tableaux\/} sem\^anticos com unifica\c c\~ao.
O programa dever\'a receber como entrada uma f\'ormula do C\'alculo de Predicados e determinar
se a mesma \'e satisfat\'{\i}vel ou n\~ao.

As regras de infer\^encia a serem utilizadas s\~ao as do C\'alculo Proposicional (regras $\alpha$
e $\beta$), acrescidas das seguintes:
\begin{enumerate}
 \item Regra $\gamma$:
       \begin{itemize}
        \item a partir de $\forall x\, A(x)$, concluir $A(v)$
        \item a partir de $\neg\exists x\, A(x)$, concluir $\neg A(v)$
       \end{itemize}
       onde $v$ \'e uma {\em nova\/} \underline{vari\'avel livre}.
 \item Regra $\delta$:
       \begin{itemize}
        \item a partir de $\exists x\, A(x)$, concluir $A(f(v_1,\ldots,v_n))$
        \item a partir de $\neg\forall x\, A(x)$, concluir $\neg A(f(v_1,\ldots,v_n))$
       \end{itemize}
       onde $f$ \'e uma {\em nova\/} \underline{fun\c c\~ao de Skolem} e $v_1$, \ldots, $v_n$
       s\~ao todas as vari\'aveis livres da f\'ormula. Se $n=0$, ou seja, se n\~ao h\'a
       vari\'aveis livres, $f$ \'e uma constante.
\end{enumerate}
Al\'em disto, o fechamento de um ramo do tableau, ao inv\'es de ocorrer quando s\~ao
encontrados literais complementares, ir\'a ocorrer quando a partir da aplica\c c\~ao
da seguinte regra (que, justamente, produz os tais literais complementares):
\begin{enumerate}
 \item[3.] Regra do fechamento:
       \begin{itemize}
        \item a partir de $A$ e $\neg B$, onde $A$ e $B$ s\~ao \'atomos, determinar o
              umg de $A$ e $B$ e aplic\'a-lo no tableau inteiro.
       \end{itemize}
\end{enumerate}

Segue um exemplo, mostrando que $\forall x(p(x)\vee q(x))\,\rightarrow\,(\forall x p(x)\vee\forall x q(x))$
n\~ao \'e v\'alida. Na Figura~\ref{ft} est\'a mostrado um trecho inicial do tableau.
\begin{figure}
\begin{center}
\begin{picture}(300,260)
 \put(150,250){\makebox(0,0){$\neg[\forall x(p(x)\vee q(x))\,\rightarrow\,(\forall x p(x)\vee\forall x q(x))]$}}
 \put(150,240){\vector(0,-1){20}}
 \put(153,230){\makebox(0,0)[l]{$\alpha$}}
 \put(150,210){\makebox(0,0){$\forall x(p(x)\vee q(x))$, $\neg(\forall x p(x)\vee\forall x q(x))$}}
 \put(150,200){\vector(0,-1){20}}
 \put(153,190){\makebox(0,0)[l]{$\alpha$}}
 \put(150,170){\makebox(0,0){$\forall x(p(x)\vee q(x))$, $\neg\forall x p(x)$, $\neg\forall x q(x)$}}
 \put(150,160){\vector(0,-1){20}}
 \put(153,150){\makebox(0,0)[l]{$\delta$}}
 \put(150,130){\makebox(0,0){$\forall x(p(x)\vee q(x))$, $\neg p(a_1)$, $\neg\forall x q(x)$}}
 \put(150,120){\vector(0,-1){20}}
 \put(153,110){\makebox(0,0)[l]{$\delta$}}
 \put(150,90){\makebox(0,0){$\forall x(p(x)\vee q(x))$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(150,80){\vector(0,-1){20}}
 \put(153,70){\makebox(0,0)[l]{$\gamma$}}
 \put(150,50){\makebox(0,0){$\forall x(p(x)\vee q(x))$, 
                            $p(v_1)\vee q(v_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(140,40){\vector(-1,-1){20}}
 \put(150,30){\makebox(0,0)[c]{$\beta$}}
 \put(160,40){\vector(1,-1){20}}
 \put(140,10){\makebox(0,0)[r]{$\forall x(p(x)\vee q(x))$, $p(v_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(160,10){\makebox(0,0)[l]{$\forall x(p(x)\vee q(x))$, $q(v_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
\end{picture}
\end{center}

\caption{\label{ft} Trecho inicial de tableau para o primeiro exemplo.}
\end{figure}
Neste instante, unificando-se $p(v_1)$ e $p(a)$ na folha da esquerda e aplicando-se o
umg em toda a \'arvore obt\'em-se (mostra-se apenas a parte modificada):
\begin{center}
\begin{picture}(300,60)
 \put(150,50){\makebox(0,0){$\forall x(p(x)\vee q(x))$,
                            $p(a_1)\vee q(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(140,40){\vector(-1,-1){20}}
 \put(150,30){\makebox(0,0)[c]{$\beta$}}
 \put(160,40){\vector(1,-1){20}}
 \put(140,10){\makebox(0,0)[r]{$\forall x(p(x)\vee q(x))$, $p(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(160,10){\makebox(0,0)[l]{$\forall x(p(x)\vee q(x))$, $q(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
\end{picture}
\end{center}
Obt\'em-se em seguida:
\begin{center}
\begin{picture}(300,90)
 \put(150,80){\makebox(0,0){$\forall x(p(x)\vee q(x))$, 
                            $p(a_1)\vee q(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(140,70){\vector(-1,-1){20}}
 \put(150,60){\makebox(0,0)[c]{$\beta$}}
 \put(160,70){\vector(1,-1){20}}
 \put(140,40){\makebox(0,0)[r]{$\forall x(p(x)\vee q(x))$, $p(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(160,40){\makebox(0,0)[l]{$\forall x(p(x)\vee q(x))$, $q(a_1)$, $\neg p(a_1)$, $\neg q(a_2)$}}
 \put(100,20){\makebox(0,0){$\bigotimes$}}
\end{picture}
\end{center}
Prosseguindo, aplica-se $\gamma$ \`a folha restante, obtendo-se:
\[\{\forall x(p(x)\vee q(x)), p(v_2)\vee q(v_2), q(a_1), \neg p(a_1), \neg q(a_2)\}\mbox{.}\]
Unificando-se $p(v_2)$ e $q(a_2)$ obt\'em-se:
\[\{\forall x(p(x)\vee q(x)), p(a_2)\vee q(a_2), q(a_1), \neg p(a_1), \neg q(a_2)\}\mbox{.}\]
Aplica-se a regra $\beta$, etc. (Como para este processo?)

Agora segue um exemplo, mostrando que $\exists w\forall x r(x,w,f(x,w))\,\rightarrow\,
 \exists w\forall x \exists y r(x,w,y)$ \'e v\'alida. Na Figura~\ref{ft2} est\'a mostrado
um trecho inicial de tableau. Observe que, neste exemplo, nas aplica\c c\~oes da regra $\gamma$ a
f\'ormula universalmente quantificada n\~ao foi copiada para n\~ao sobrecarregar as figuras.
Considere que toda f\'ormula universalmente quantificada (com $\forall$ ou $\neg\exists$
como prefixo), est\'a presente em todos os nodos filhos no tableau!
\begin{figure}
\begin{center}
\begin{picture}(300,260)
 \put(150,250){\makebox(0,0){$\neg[\exists w\forall x r(x,w,f(x,w))\,\rightarrow\,
                                \exists w\forall x \exists y r(x,w,y)]$}}
 \put(150,240){\vector(0,-1){20}}
 \put(153,230){\makebox(0,0)[l]{$\alpha$}}
 \put(150,210){\makebox(0,0){$\exists w\forall x r(x,w,f(x,w))$, $\neg \exists w\forall x \exists y r(x,w,y)$}}
 \put(150,200){\vector(0,-1){20}}
 \put(153,190){\makebox(0,0)[l]{$\delta$}}
 \put(150,170){\makebox(0,0){$\forall x r(x,a_1,f(x,a_1))$, $\neg \exists w\forall x \exists y r(x,w,y)$}}
 \put(150,160){\vector(0,-1){20}}
 \put(153,150){\makebox(0,0)[l]{$\gamma$}}
 \put(150,130){\makebox(0,0){$\forall x r(x,a_1,f(x,a_1))$, $\neg\forall x \exists y r(x,v_1,y)$}}
 \put(150,120){\vector(0,-1){20}}
 \put(153,110){\makebox(0,0)[l]{$\delta$}}
 \put(150,90){\makebox(0,0){$\forall x r(x,a_1,f(x,a_1))$, $\neg\exists y r(f_1(v_1),v_1,y)$}}
 \put(150,80){\vector(0,-1){20}}
 \put(153,70){\makebox(0,0)[l]{$\gamma$}}
 \put(150,50){\makebox(0,0){$r(v_2,a_1,f(v_2,a_1))$, $\neg\exists y r(f_1(v_1),v_1,y)$}}
 \put(150,40){\vector(0,-1){20}}
 \put(153,30){\makebox(0,0)[l]{$\gamma$}}
 \put(150,10){\makebox(0,0){$r(v_2,a_1,f(v_2,a_1))$, $\neg r(f_1(v_1),v_1,v_3)$}}
\end{picture}
\end{center}

\caption{\label{ft2} Trecho inicial de tableau para o segundo exemplo.}
\end{figure}
Fazendo-se a unifica\c c\~ao, obt\'em-se (mostrando apenas a parte modificada):
\begin{center}
\begin{picture}(300,160)
 \put(150,150){\makebox(0,0){$\forall x r(x,a_1,f(x,a_1))$, $\neg\forall x \exists y r(x,a_1,y)$}}
 \put(150,140){\vector(0,-1){20}}
 \put(153,130){\makebox(0,0)[l]{$\delta$}}
 \put(150,110){\makebox(0,0){$\forall x r(x,a_1,f(x,a_1))$, $\neg\exists y r(f_1(a_1),a_1,y)$}}
 \put(150,100){\vector(0,-1){20}}
 \put(153,90){\makebox(0,0)[l]{$\gamma$}}
 \put(150,70){\makebox(0,0){$r(f_1(a_1),a_1,f(f_1(a_1),a_1))$, $\neg\exists y r(f_1(a_1),a_1,y)$}}
 \put(150,60){\vector(0,-1){20}}
 \put(153,50){\makebox(0,0)[l]{$\gamma$}}
 \put(150,30){\makebox(0,0){$r(f_1(a_1),a_1,f(f_1(a_1),a_1))$, $\neg r(f_1(a_1),a_1,f(f_1(a_1),a_1))$}}
 \put(150,10){\makebox(0,0){$\bigotimes$}}
\end{picture}
\end{center}

Para fazer este trabalho, basta estender o que foi feito no primeiro trabalho. Uma outra op\c c\~ao
\'e fazer tudo usando a linguagem Prolog. Neste caso, uma refer\^encia \'util \'e:
\begin{itemize}
 \item Fitting, M., {\em First-Order Logic and Automated Theorem Proving\/}, 2nd ed., Springer, 1996.
\end{itemize}
Este livro cont\'em o c\'odigo em Prolog para uma vers\~ao do que est\'a sendo pedido neste trabalho,
na Se\c c\~ao 7.5. Tal c\'odigo pode ser obtido na p\'agina da disciplina (veja a parte
relativa \`as p\'aginas 169 a 183). Se voc\^e aproveitar este c\'odigo do Fitting, estenda-o para
determinar, para f\'ormulas satisfat\'{\i}veis, pelo menos uma interpreta\c c\~ao que a satisfaz. Use
isso para, ao determinar se uma f\'ormula \'e v\'alida, exibir uma interpreta\c c\~ao que n\~ao a
satisfaz quando ela n\~ao for v\'alida.

Seguem algumas f\'ormulas v\'alidas que podem ser usadas para teste do programa, tirados do livro
do M. Fitting (Exerc\'{\i}cio 7.4.1, p\'ag. 169):
\begin{enumerate}
 \item $\exists x\forall y\, r(x,y) \,\rightarrow\, \forall y\exists x\, r(x,y)$
 \item $\exists x\,(p(x) \,\rightarrow\, \forall x\, p(x))$
 \item $\forall x\forall y\, (p(x)\wedge p(y)) \,\rightarrow\, \exists x\exists y\,(p(x)\vee p(y))$
 \item $\forall x\forall y\, (p(x)\wedge p(y)) \,\rightarrow\, \forall x\forall y\,(p(x)\vee p(y))$
 \item $\forall x\exists y\forall z\exists w\, (r(x,y)\vee \neg r(w,z))$
 \item $\forall x\, q(x) \,\rightarrow\, \exists x\forall y\, [p(y)\uparrow(p(x)\uparrow q(x))]$
\end{enumerate}

\end{document}
