\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\^{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 Exame especial} \hfill \textbf{Duração: 1h 40min} \hfill 14/12/2011

\vspace*{3mm}
\begin{enumerate}
 \item Mostre que $(p \rightarrow q)\rightarrow r\equiv (\neg p \rightarrow r)\wedge(q\rightarrow r)$ utilizando equival\^encias mais simples, explicitando todas as equival\^encias as utilizadas.
 \item Para a f\'ormula $(\neg p\vee q\leftrightarrow (p\wedge q$,
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Mostre a \'arvore e-ou correspondente \`a chamada de \textsf{sat$\downarrow$b}.
        \item Construa uma árvore de computação para aplicação de \textsf{sat}$\downarrow$\textsf{bf}.
        \item Para a árvore obtida, escolha um dos ramos de \emph{sucesso} mais curtos e exiba o conjunto
              de partida e a derivação correspondentes que demonstrem que a fórmula é satisfatível.
       \end{list}
 \item Mostre que $H\models\{\alpha\}$ se, e somente se, $H\cup\{\neg\alpha\}$ é inconsistente.
 \item Demonstre por meio de tableaux marcados:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item $\{\}\vdash p\wedge q\rightarrow p\vee q$
        \item $\{p\rightarrow(q\rightarrow r)\}\vdash p\wedge q\rightarrow r$
       \end{list}
 \item Expresse em l\'ogica de predicados:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item Nem tudo que reluz \'e ouro.
        \item Quem gosta de Pedrinho n\~ao o conhece.
        \item Juca adormece se e somente se a luz fica acesa.
        \item Ningu\'em visita Hermengarda, a menos que ela esteja af\^onica.
        \item Todos amam quem ama algu\'em.
       \end{list}
 \item Determine $\sigma \circ \theta$ para:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\sigma = \{x/f(y), z/f(w)\}$, $\theta = \{y/a, z/f(a)\}$
        \item $\sigma = \{x/y, z/f(g(x,y))\}$, $\theta = \{x/y, y/a, z/a\}$
       \end{list}
 \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(v,z,v)\vee p(w,z,w)$ e $p(w,h(x,x),w)$
       \end{list}
 \item Sejam os seguintes fatos:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Todos que entraram no pa\'{\i}s e n\~{a}o eram VIPs foram
              revistados por um agente da pol\'{\i}cia federal.
        \item Paulo C. era contrabandista.
        \item Paulo C. entrou no pa\'{\i}s.
        \item Paulo C. s\'{o} foi revistado por contrabandistas.
        \item Nenhum contrabandista era VIP.
       \end{list}
       Utilizando resolu\c{c}\~{a}o com extra\c{c}\~{a}o de respostas, encontre
       uma pessoa que era, ambos, contrabandista e agente da pol\'{\i}cia
       federal.
\end{enumerate}

\end{document}
