\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} \hfill \textbf{Duração: 1h 40min} \hfill 27/06/2013

\vspace*{3mm}
\begin{enumerate}
 \item 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$.
 \item 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}
 \item 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}
 \item 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}
% \item Mostre que $\forall x (\alpha(x)\wedge\beta(x))\equiv \forall x \alpha(x)\wedge\forall x\beta(x)$.
 \item 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$.
 \item 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).
\end{enumerate}

\vspace*{3mm}
\hrule
\vspace*{.5mm}
\hrule
\vfill
 No verso estão as regras lógicas do sistema ${\cal S}_G$.
\vfill
\newpage
\textbf{Regras lógicas do sistema formal ${\cal S}_G$}:
 \begin{center}
  \[\begin{array}{rcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum}}\\
     \textsf{vere}: & \Psi_1\vdash\Psi_2  & \textsf{verd}: &   \\
                    & \overline{\Psi_1,\top\vdash\Psi_2} &  & \overline{\Psi_1\vdash\top,\Psi_2} \\
     \multicolumn{4}{l}{\mbox{\sf Falsum}}\\
     \textsf{fale}: &                      & \textsf{fald}: &  \Psi_1\vdash\Psi_2 \\
                    & \overline{\Psi_1,\bot\vdash\Psi_2} &  & \overline{\Psi_1\vdash\bot,\Psi_2} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
     \textsf{nege}: & \Psi_1\vdash\alpha,\Psi_2 & \textsf{negd}: & \Psi_1,\alpha\vdash\Psi_2 \\
             & \overline{\Psi_1,\neg\alpha\vdash\Psi_2} &        & \overline{\Psi_1\vdash\neg\alpha,\Psi_2} \\
     \multicolumn{4}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conje}: & \Psi_1,\alpha,\beta\vdash\Psi_2 & \textsf{conjd}: & \Psi_1\vdash\alpha,\Psi_2
                     \hspace*{3mm}\Psi_1\vdash\beta,\Psi_2\\
       & \overline{\Psi_1,\alpha\wedge\beta\vdash\Psi_2}& & \overline{\hspace*{7mm}\Psi_1\vdash\alpha\wedge\beta,\Psi_2\hspace*{7mm}} \\
     \multicolumn{4}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disje}: & \Psi_1,\alpha\vdash\Psi_2\hspace*{3mm}\Psi_1,\beta\vdash\Psi_2 & \textsf{disjd}: & \Psi_1\vdash\alpha,\beta,\Psi_2 \\
                     & \overline{\hspace*{7mm}\Psi_1,\alpha\vee\beta\vdash\Psi_2\hspace*{7mm}}& & \overline{\Psi_1\vdash\alpha\vee\beta,\Psi_2} \\
     \multicolumn{4}{l}{\mbox{\sf Condicional}} \\
     \textsf{conde}: & \Psi_1\vdash\alpha,\Psi_2 \hspace*{3mm}\Psi_1,\beta\vdash\Psi_2 & \textsf{condd}: & \Psi_1,\alpha\vdash\beta,\Psi_2 \\
                     & \overline{\hspace*{7mm}\Psi_1,\alpha\rightarrow\beta\vdash\Psi_2\hspace*{7mm}}& & \overline{\Psi_1\vdash\alpha\rightarrow\beta,\Psi_2} \\
     \multicolumn{4}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bice}: & \Psi_1,\alpha,\beta\vdash\Psi_2\hspace*{5mm}\Psi_1\vdash\alpha,\beta,\Psi_2 & \textsf{bicd}: & \Psi_1,\alpha\vdash\beta,\Psi_2 \hspace*{5mm}\Psi_1,\beta\vdash\alpha,\Psi_2 \\
                    & \overline{\hspace*{11mm}\Psi_1,\alpha\leftrightarrow\beta\vdash\Psi_2\hspace*{11mm}}& & \overline{\hspace*{11mm}\Psi_1\vdash\alpha\leftrightarrow\beta,\Psi_2\hspace*{11mm}}
    \end{array}
  \]
 \end{center}

\end{document}
