\documentclass[11pt,a4paper]{report}

\usepackage[brazil]{babel}
\usepackage[latin1] {inputenc}
\usepackage{fullpage}

%\usepackage{gastex}
%\usepackage[usenames]{color}

\newcounter{conta}
\pagestyle{empty}

\begin{document}

\noindent Departamento de Ciência da Computaçãoo
\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 Exame Especial} \hfill \textbf{Duração: 1h 40min} \hfill 10/7/2013

\vspace*{3mm}
\begin{enumerate}
 \item Defina o que é:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Equivalência lógica.
				\item Consequência lógica.
       \end{list}

 \item Explique como os problemas de determinar se uma fórmula é
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item satisfatível;
        \item tautologia;
       \end{list}
       podem ser reduzidos ao de determinar se uma fórmula é falseável. (Basta dizer, no caso de (a):
			 $\alpha$ é satisfatível sse \ldots é falseável; analogamente para os outros dois ítens.)

 \item Seja $\alpha=(p\rightarrow q)\wedge\neg(p\wedge\neg r)$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Apresente uma derivação de $\alpha$ em ${\cal S}_A$ ou ${\cal S}_B$.
        \item Dê uma condição necessária e suficiente para que uma interpretação seja um modelo de $\alpha$.
       \end{list}       

 \item Expresse em lógica de predicados:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item \emph{Quem faz exercícios tem melhor qualidade de vida.} \\ Predicados unários: \textsf{ex} (faz exercícios
				      físicos); \textsf{qual} (tem melhor qualidade de vida).
        
%              $\forall x (\textsf{ex}(x)\rightarrow\textsf{qual}(x))$
        \item \emph{Nenhum amigo de Carlos gosta da mãe (de Carlos).} Predicados binários: \textsf{amigo}, \textsf{gosta}.
				      Função: \textsf{mãe}.
        
%              $\neg \exists x (\textsf{amigo}(\textsf{Carlos},x)\wedge\textsf{gosta}(x,\textsf{mae}(\textsf{Carlos})))$
        \item \emph{Gatos não se dão bem com cachorros. e vice-versa}. \\ Predicados unários: \textsf{gato},
				      \textsf{cachorro}. Predicado binário: \textsf{bem} (se dá bem com).

%              $\forall x \forall y((\textsf{gato}(x)\wedge\textsf{cachorro}(y))\vee (\textsf{cachorro}(x)\wedge\textsf{gato}(y))\rightarrow \neg \textsf{bem}(x,y))$
       \end{list}

 \item Mostre que $\exists x(p(x)\rightarrow q(x))\rightarrow(\exists x p(x)\rightarrow\exists x q(x))$ não é válida.

 \item Encontre todos os resolventes dos seguintes pares de cl\'{a}usulas:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item  $\neg p(x) \vee q(x,b)$ e $p(a)\vee q(a,b)$
        \item  $\neg p(x)\vee q(x, x)$ e $\neg q(a,f(a))$
 %       \item  $\neg p(x,y,u)\vee\neg p(y,z,v)\vee\neg p(x,v,u)\vee p(u,z,w)$ e $p(g(x,y),x,y)$
        \item  $\neg p(v,z,v)\vee p(w,z,w)$ e $p(w,h(x,x),w)$
       \end{list}

\end{enumerate}

\vspace*{3mm}
\hrule

\vspace{.5mm}
\hrule

\vspace{5mm}
No verso, as regras do sistema formal ${\cal S}_A$.

\newpage
\begin{flushleft} \bf\large
As regras do sistema formal ${\cal S}_A$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrcrcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum e falsum}}\\
     \textsf{verp}: &                & \textsf{faln}: &  \\
                    &\overline{V\top}&                & \overline{F\bot} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
     \textsf{negp}: & F \alpha  & \textsf{negn}: &V \alpha \\
                    & \overline{V\neg\alpha}& & \overline{F \neg\alpha} \\
     \multicolumn{6}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & V\alpha \ \ V\beta           & \textsf{conjn1}: & F \alpha & \textsf{conjn2}: & F \beta \\
                     & \overline{V\alpha\wedge\beta}& & \overline{F \alpha\wedge\beta} & &\overline{F \alpha\wedge\beta} \\
     \multicolumn{6}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp1}: & V\alpha    & \textsf{disjp2}: & V \beta & \textsf{disjn}: & F \alpha\ \ F\beta \\
                     & \overline{V\alpha\vee\beta}& & \overline{V\alpha\vee\beta} & &\overline{F \alpha\vee\beta} \\
     \multicolumn{6}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp1}: & F\alpha    & \textsf{condp2}: & V \beta & \textsf{condn}: & V \alpha\ \ F\beta \\
                     & \overline{V\alpha\rightarrow\beta}& & \overline{V\alpha\rightarrow\beta} & &\overline{F \alpha\rightarrow\beta} \\
     \multicolumn{8}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp1}: & V\alpha\ \ V\beta & \textsf{bicp2}: & F\alpha\ \ F\beta & \textsf{bicn1}: & V \alpha\ \ F\beta & \textsf{bicn2}: & F \alpha\ \ V\beta \\
                     & \overline{V\alpha\leftrightarrow\beta}& & \overline{V\alpha\leftrightarrow\beta} & &\overline{F \alpha\leftrightarrow\beta}& &\overline{F \alpha\leftrightarrow\beta}
    \end{array}
  \]
 \end{center}


\end{document}
