\documentclass[11pt,a4paper]{book}

\usepackage[brazil]{babel}
\usepackage[latin1] {inputenc}
\usepackage{fullpage}
\pagestyle{empty}
%\usepackage{gastex}
%\usepackage[usenames]{color}

\newcounter{conta}
\pagestyle{empty}

\begin{document}

\vspace*{1cm}
\noindent Departamento de Ciência da Computação \hfill ICEx/UFMG \\
\noindent {\it Lógica Aplicada a Computação}
\hfill $\mbox{1}^{\mbox{\underline{o}}}$ semestre de 2013 \\
\noindent Professor: Newton José Vieira \\
\noindent {\bf Segunda Prova}/Solução do professor  \hfill 27/06/2013

\vspace*{3mm}
\begin{enumerate}
 \item {\footnotesize Suponha que você tenha algoritmos para determinar, dada uma fórmula, se ela é:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item tautologia;
        \item satisfatível.
       \end{list}
       Explique como você poderia utilizar cada um desses dois algoritmos para determinar, dados um conjunto
			 finito de fórmulas $H$ e uma fórmula $\alpha$, se $H\models \alpha$.}

       \emph{Solução}:

        Seja $H=\{\beta_1,\ldots,\beta_n\}$. Para determinar se $H\models \alpha$:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Verificar se $(\beta_1\wedge\ldots\wedge\beta_n)\rightarrow\alpha$ é tautologia, $n>0$.
              Se $n=0$, verificar se $\alpha$ é tautologia.
        \item Verificar se $(\beta_1\wedge\ldots\wedge\beta_n)\wedge\neg\alpha$ não é satisfatível, $n>0$.
              Se $n=0$, verificar se $\neg\alpha$ não é satisfatível.
       \end{list}

 \item {\footnotesize Encontre deduções no sistema formal ${\cal S}_G$ para os seguintes sequentes:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item $\vdash\neg\neg p\rightarrow p$
        \item $\vdash ((p\rightarrow\bot)\rightarrow\bot)\leftrightarrow p$
       \end{list}}

       \emph{Solução}:

       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item \begin{tabbing}
               xxxx\= 4. $\vdash\neg\neg p\rightarrow p$ \ \=\kill
                 \> 1. $p \vdash p$ \> (\textsf{Ax}) \\
                 \> 2. $\vdash \neg p,p$ \> (\textsf{negd} 1) \\
                 \> 3. $\neg\neg p\vdash p$ \> (\textsf{nege} 2) \\
                 \> 4. $\vdash \neg\neg p\rightarrow p$ \> (\textsf{condd} 3)
              \end{tabbing}
        \item \begin{tabbing}
               xxxx\= 4. $\vdash ((p\rightarrow\bot)\rightarrow\bot)\leftrightarrow p$ \ \=\kill
                 \> 1. $p\vdash \bot,p$ \> (\textsf{Ax}) \\
                 \> 2. $\vdash p\rightarrow\bot,p$ \> (\textsf{condd} 1) \\
                 \> 3. $\bot\vdash p$ \> (\textsf{fale}) \\
                 \> 4. $(p\rightarrow\bot)\rightarrow\bot\vdash p$ \> (\textsf{conde} 2,3) \\
                 \> 5. $p\vdash p,\bot$ \> (\textsf{Ax}) \\
                 \> 6. $p,\bot\vdash \bot$ \> (\textsf{fale}) \\
                 \> 7. $p,p\rightarrow\bot\vdash \bot$ \> (\textsf{conde} 5,6) \\
                 \> 8. $p\vdash (p\rightarrow\bot)\rightarrow\bot$ \> (\textsf{condd} 7) \\
                 \> 9. $\vdash ((p\rightarrow\bot)\rightarrow\bot)\leftrightarrow p$ \> (\textsf{bicd} 4,8)
              \end{tabbing}
       \end{list}

\newpage
 \item {\footnotesize Encontre deduções lineares, em resolução, que demonstrem as consequências:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item $\{p\rightarrow q$$,(q\vee \neg r_1)\rightarrow(r_2\wedge \neg s),p\}\models \neg s$.
        \item $\{(p\vee s_1)\rightarrow(q\rightarrow s_2),(p\vee r_1)\rightarrow(s_2\rightarrow s_3),
               p\wedge\neg r_3\}\models q\rightarrow s_3$.
       \end{list}}

       \emph{Solução}:

       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item \begin{tabbing}
               xxx\=10. $\neg q\vee \neg s$xx\= \kill
                  \>1. $\neg p\vee q$       \>($B$) \\
                  \>2. $\neg q\vee r_2$     \>($B$) \\
                  \>3. $\neg q\vee \neg s$  \>($B$) \\
                  \>4. $r_1\vee r_2$        \>($B$) \\
                  \>5. $r_1\vee \neg s$     \>($B$) \\
                  \>6. $p$                  \>($B$) \\
                  \>7. $s$                  \>(\textsf{nc}) \\
                  \>8. $\neg q$             \>(7,3) \\
                  \>9. $\neg p$             \>(8,1) \\
                  \>10. $\bot$              \>(9,6)
              \end{tabbing}
        \item \begin{tabbing}
               xxx\=10. $\neg s_1\vee \neg q_2\vee s_2$xx\= \kill
                  \>1. $\neg p\vee \neg q\vee s_2$       \>($B$) \\
                  \>2. $\neg s_1\vee \neg q\vee s_2$     \>($B$) \\
                  \>3. $\neg p\vee \neg s_2\vee s_3$     \>($B$) \\
                  \>4. $\neg r_1\vee \neg s_2\vee s_3$   \>($B$) \\
                  \>5. $p$                               \>($B$) \\
                  \>6. $\neg r_3$                        \>($B$) \\
                  \>7. $q$                               \>(\textsf{nc}) \\
                  \>8. $\neg s_3$                        \>(\textsf{nc}) \\
                  \>9. $\neg p\vee \neg s_2$             \>(8,3) \\
                  \>10. $\neg p\vee\neg q$               \>(9,1) \\
                  \>11. $\neg q$                         \>(10,5) \\
                  \>12. $\bot$                           \>(11,7)
              \end{tabbing}
       \end{list}
 \item {\footnotesize Expresse em lógica de predicados:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item \emph{Nem tudo que reluz é ouro}. \\ Predicados unários: reluz e é-ouro.
        \item \emph{Quem gosta de Pedrinho n\~ao o conhece.} \\ Predicados binários: gosta e conhece.
        \item \emph{Gatos e cachorros atacam se s\~ao amea\c{c}ados}. \\ Predicados unários: gato, cachorro, ameaçado e ataca.
        \item \emph{Todos amam quem ama algu\'em.} \\ Predicado binário: ama.
       \end{list}}

       \emph{Solução}:

       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item $\exists x (\mbox{reluz}(x)\wedge\neg\mbox{ouro}(x))$
        \item $\forall x(\mbox{gosta}(x,\mbox{Pedrinho})\rightarrow\neg \mbox{conhece}(x,\mbox{Pedrinho})))$
        \item $\forall x[((\mbox{gato}(x)\vee \mbox{cachorro}(x))\rightarrow(\mbox{ameaçado}(x)\rightarrow
               \mbox{ataca}(x))]$
        \item $\forall x\forall y((\exists z\, \mbox{ama}(y,z))\rightarrow\mbox{ama}(x,y))$
      \end{list}

\newpage
% \item Mostre que $\forall x (\alpha(x)\wedge\beta(x))\equiv \forall x \alpha(x)\wedge\forall x\beta(x)$.
 \item {\footnotesize Mostre que $\forall x (\alpha(x)\vee\beta(x))\not\equiv \forall x \alpha(x)\vee\forall x\beta(x)$. \\
       $\alpha(x)$ é uma fórmula cuja única variável livre é $x$.}

       \emph{Solução}:

       Uma interpretação com universo $\{e_1,e_2\}$ e tal que $v^i(\alpha(x))=V$ para $x^i=e_1$,
		   $v^i(\alpha(x))=F$ para $x^i=e_2$, $v^i(\beta(x))=F$ para $x^i=e_1$ e $v^i(\beta(x))=V$ para $x^i=e_2$,
			 satisfaz $\forall x (\alpha(x)\vee\beta(x))$, mas não satisfaz $\forall x \alpha(x)\vee\forall x\beta(x)$.
			 Logo, $\forall x (\alpha(x)\vee\beta(x))\not\equiv\forall x \alpha(x)\vee\forall x\beta(x)$.

 \item {\footnotesize Seja o argumento:
       \begin{quote}
        \emph{Todos amam quem ama algu\'em. Existe algu\'em que n\~ao ama a si mesmo. Portanto, algu\'em n\~ao me ama.}
       \end{quote}
       Expresse-o em lógica de predicados e mostre que ele é válido. Caso queira, pode usar um sistema formal
			 (tableaux, resolução , \ldots).}

       \emph{Solução}:

        O argumento diz:
				$$\{\forall x\forall y((\exists z\, \mbox{ama}(y,z))\rightarrow\mbox{ama}(x,y)),
				  \exists x \neg \mbox{ama}(x,x))\}\models \exists x\neg \mbox{ama}(x,\mbox{eu})\mbox{.}$$
				Usando resolução:
				\begin{tabbing}
				 xxx\= $1.\neg\mbox{ama}(y,z)\vee\mbox{ama}(x,y)$xx \= \kill
				    \> 1. $\neg\mbox{ama}(y,z)\vee\mbox{ama}(x,y)$  \> (primeira premissa) \\
			      \> 2. $\neg\mbox{ama}(a,a)$                     \> (segunda premissa) \\
			      \> 3. $\mbox{ama}(x,\mbox{eu})$                 \> (negação da conclusão) \\
			      \> 4. $\mbox{ama}(x,y)$                         \> (3,1) \\
			      \> 5. $\bot$                                    \> (4,2)
				\end{tabbing}
				Logo, o argumento é válido.
\end{enumerate}

\end{document}