\documentclass[11pt, a4paper]{report}

\usepackage[portuguese]{babel}
\usepackage{fullpage}
\pagestyle{empty}
\newcounter{conta}
\usepackage{gastex}
\usepackage[usenames]{color}

\begin{document}

\vspace*{1cm}
\noindent {\it Automa\c{c}\~ao de Sistemas de Infer\^encia}
\hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2008 \\
\noindent Professor: Newton Jos\'{e} Vieira \hfill DCC/ICEx/UFMG \\
\noindent {\bf Primeira Prova} \hfill {9/10/2008}

\vspace*{1mm}
\noindent \textbf{Dura\c{c}\~ao:} 1 hora e 30 minutos. \\

\vspace*{2mm}
\begin{enumerate}

 \item Seja $\alpha=(p\vee q)\rightarrow(p\rightarrow q)$ e sejam $i(p)=V$ e $i(q)=F$.
        \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Avalie $v^i(\alpha)$ usando a defini\c{c}\~ao recursiva de $v^i$.
        \item Apresente o grafo de $\alpha$ com os valores propagados pelo procedimento avalia.
        \item Simplifique $\alpha$, como o procedimento avaliaf, em dois passos:
              \begin{enumerate}
               \item[1.] aplicando a substitui\c{c}\~ao $p/\top$;
               \item[2.] aplicando a substitui\c{c}\~ao $q/\bot$.
              \end{enumerate}
       \end{list}

 \item Como um algoritmo para testar se uma f\'ormula \'e satisfaz\'{\i}vel pode ser usado para
       determinar se:
        \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item as f\'ormulas $\alpha$ e $\beta$ s\~ao tais que $\alpha\equiv\beta$?
        \item $\{\alpha_1,\alpha_2,\ldots,\alpha_n\}\models\beta$?
       \end{list}

 \item O problema de determinar se uma f\'ormula \'e satisfaz\'{\i}vel pode ser reduzido ao de determinar
       se uma f\'ormula \'e \textit{tautologia}, j\'a que: \[\alpha \mbox{ \'e satisfaz\'{\i}vel se, e somente se, }
       \neg \alpha \mbox{ n\~ao \'e \textit{tautologia}.}\]
       De forma an\'aloga, mostre que os problemas de determinar se uma f\'ormula \'e:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item satisfaz\'{\i}vel,
        \item false\'avel,
        \item tautologia, e
        \item conting\^encia
       \end{list}
       podem ser reduzidos ao de determinar se uma f\'ormula \'e uma \textit{contradi\c{c}\~ao}.

 \item Seja a f\'ormula $\gamma=(p\leftrightarrow\bot)\wedge(\neg p\rightarrow q)$. Apresente:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item a \'arvore e-ou para satisfa\c{c}\~ao de $\gamma$;
        \item os conjuntos \textit{ints} anotados ao lado de cada v\'ertice da \'arvore e-ou;
        \item uma f\'ormula na forma normal disjuntiva equivalente a $\gamma$ obtida a partir do \textit{ints}
              anotado ao lado da raiz da \'arvore e-ou.
       \end{list}

\end{enumerate}

\end{document}

