\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}
\noindent Departamento de Ci\^{e}ncia da Computa\c{c}\~{a}o \hfill ICEx/UFMG \\
\noindent {\it Lógica Aplicada a Computação} \hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2011 \\
\noindent Professor: Newton Jos\'{e} Vieira \\
\noindent {\bf Primeira Prova}/Especial \hfill \textbf{Dura\c{c}\~ao: 1h 40min} \hfill 31/10/2011

\vspace{2mm}

\begin{enumerate}
 \item Seja $\varphi=((p\rightarrow \neg q)\vee r)\wedge (\neg r\wedge(p\rightarrow \neg q))$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Desenhe o grafo simplificado de $\varphi$.
        \item Apresente um modelo para $\varphi$, se houver algum. Se não houver, mostre que não há.
        \item Derive $\top$ ou $\bot$ a partir da avaliação de $\varphi$ para $i(p)=V$, $i(q)=V$, $i(r)=F$,
              usando as regras de re-escrita abaixo, se possível. Se não for possível, diga a razão.
              \begin{quote}
               \textsf{neg1}: $\neg\top\mapsto\bot$ \\
               \textsf{neg2}: $\neg\bot\mapsto\top$ \\
               \textsf{con1}: $\alpha\wedge\top\mapsto\alpha$ \\
               \textsf{con1}: $\alpha\wedge\bot\mapsto\bot$ \\
               \textsf{dis1}: $\alpha\vee\top\mapsto\top$ \\
               \textsf{dis1}: $\alpha\vee\bot\mapsto\alpha$ \\
               \textsf{cond}: $\alpha\rightarrow\beta\mapsto\neg\alpha\vee\beta$
              \end{quote}
       \end{list}
 \item Faça definições precisas (como foi feito na apostila) dos seguintes conceitos:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Equivalência lógica.
        \item Tautologia.
        \item Modelo.
       \end{list}
 \item Mostre que sim ou que n\~ao:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Se $\alpha\wedge\beta$ \'e satisfat\'{\i}vel, ent\~ao $\beta$ \'e satisfat\'{\i}vel.
        \item Se $\alpha\vee\beta$ \'e satisfat\'{\i}vel, ent\~ao $\beta$ \'e satisfat\'{\i}vel.
        \item Se $\alpha$ \'e satisfat\'{\i}vel, ent\~ao $\neg\alpha$ \'e insatisfat\'{\i}vel.
       \end{list}
 \item Seja $\psi=(p\leftrightarrow\neg q)\rightarrow(p\vee q)$.
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Mostre a \'arvore e-ou correspondente a \textsf{sat$\downarrow$($\psi$)} ou
              \textsf{sat$\downarrow$b($\psi$)}.
        \item Determine o conjunto \textit{ints} para cada vértice da árvore.
        \item Exiba os modelos de $\psi$ indicados por \textit{ints}.
       \end{list}
 \item Ainda para $\psi=(p\leftrightarrow\neg q)\rightarrow(p\vee q)$:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Mostre a árvore de computação correspondente a \textsf{sat$\downarrow$bf($\psi$)}.
        \item Escolha uma ramo da árvore e apresente a derivação correspondente de $\psi$ a partir
              de um conjunto de partida. Explicite cada regra de derivação usada.
       \end{list}
\end{enumerate}

\end{document}