\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 Primeira Prova} \hfill \textbf{Duração: 1h 40min} \hfill 18/10/2011

\vspace*{3mm}
\begin{enumerate}
 \item Seja $\alpha=((p\rightarrow q)\vee r)\rightarrow (\neg q\wedge(p\vee r))$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Desenhe o grafo simplificado de $\alpha$.
        \item Avalie $\alpha$ para $i(p)=V$, $i(q)=F$, $i(r)=F$, anotando junto aos vértices do grafo de
              $\alpha$ o valor da subfórmula associada para esta interpretação.
       \end{list}

 \item Seja o conjunto de 7 regras:
       \begin{itemize}
        \item Negação: $\neg\top\mapsto\bot$ (\textsf{neg1}) e $\neg\bot\mapsto\top$ (\textsf{neg2}).
        \item Conjunção: $\top\wedge\alpha\mapsto\alpha$ (\textsf{conj1}) e $\bot\wedge\alpha\mapsto\bot$
              (\textsf{conj2}).
        \item Disjunção: $\top\vee\alpha\mapsto\top$ (\textsf{disj1}) e $\bot\vee\alpha\mapsto\alpha$ (\textsf{disj2}).
        \item Condicional: $\alpha\rightarrow\beta\mapsto\neg\alpha\vee\beta$ (\textsf{cond}).
       \end{itemize}
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Apresente uma derivação de $\top$ ou de $\bot$ a partir de $(\top\rightarrow \bot)\vee
             ((\neg \top\rightarrow \bot)\wedge\neg \top)$.
        \item Dada uma fórmula $\alpha$ com apenas os conectivos $\top$, $\bot$, $\neg$, $\wedge$,
              $\vee$ e $\rightarrow$, sem variáveis (isto é, cujos elementos mais simples são $\top$ e/ou $\bot$),
              é possível avaliar $\alpha$ (isto é, derivar $\top$ ou $\bot$) usando apenas essas 7 regras.
              Formule uma regra para a Bicondicional (apenas uma), de forma a preservar tal propriedade
              (agora para 8 regras).
       \end{list}

 \item Explique como os problemas de determinar se uma f\'ormula pertence a cada uma das 4
       classes de f\'ormulas, satisfatíveis, falseáveis, tautologias e contingências, podem ser reduzidos ao de
       determinar se uma f\'ormula \'e uma contradi\c c\~ao.

 \item Seja $\alpha=((p\rightarrow q)\wedge r)\rightarrow (\neg q\wedge(p\vee r))$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Apresente uma árvore e-ou para satisfação de $\alpha$ (pode escolher a de \textsf{sat$\downarrow$} ou
              de  \textsf{sat$\downarrow$b}).
        \item Anote na árvore e-ou os conjuntos \textit{ints} de cada vértice.
        \item Que modelos sugerem o conjunto \textit{ints} correspondente a $\alpha$?
       \end{list}

 \item Seja $\alpha=(p\leftrightarrow q)\wedge \neg(p\vee q)$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Apresente uma árvore de computação para satisfação de $\alpha$ via \textsf{sat$\downarrow$f} ou
              de  \textsf{sat$\downarrow$bf}.
        \item Escolha um ramo da árvore que corresponda a satisfação de $\alpha$ e escreva uma
              derivação de $\alpha$ a partir do conjunto de partida pertinente.
        \item O conjunto de partida usado em (b) corresponde a que modelo?
       \end{list}
       (Veja no verso as regras do sistema formal para satisfabilidade com fórmulas marcadas.)
\end{enumerate}

\pagebreak
\textbf{Regras do sistema formal para satisfabilidade com fórmulas marcadas}:
 \begin{center}\setlength{\unitlength}{1mm}
  \begin{picture}(70,12)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \put(5,8){\line(1,0){14}}
   \put(0,8){\makebox(0,0){(0)}}
   \node(1)(12,5){$V \top$}

   \put(30,8){\line(1,0){14}}
   \node(3)(37,5){$F \bot$}
  \end{picture}

  \begin{picture}(70,15)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \node(0)(12,11){$F \gamma$}
   \put(5,8){\line(1,0){14}}
   \put(0,8){\makebox(0,0){(1)}}
   \node(1)(12,5){$V \neg\gamma$}

   \node(2)(37,11){$V \gamma$}
   \put(30,8){\line(1,0){14}}
   \node(3)(37,5){$F \neg\gamma$}
  \end{picture}

  \begin{picture}(70,15)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \node(0)(7,11){$V \gamma_1$}
   \node(1)(17,11){$V \gamma_2$}
   \put(5,8){\line(1,0){14}}
   \put(0,8){\makebox(0,0){(2)}}
   \node(2)(12,5){$V \gamma_2\wedge\gamma_2$}

   \node(3)(37,11){$F \gamma_1$}
   \put(30,8){\line(1,0){14}}
   \node(4)(37,5){$F \gamma_1\wedge\gamma_2$}

   \node(5)(57,11){$F \gamma_2$}
   \put(50,8){\line(1,0){14}}
   \node(6)(57,5){$F \gamma_1\wedge\gamma_2$}
  \end{picture}

  \begin{picture}(70,15)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \node(0)(12,11){$V \gamma_1$}
   \put(5,8){\line(1,0){14}}
   \node(1)(12,5){$V \gamma_1\vee\gamma_2$}
   \put(0,8){\makebox(0,0){(3)}}

   \node(2)(32,11){$V \gamma_2$}
   \put(25,8){\line(1,0){14}}
   \node(3)(32,5){$V \gamma_1\vee\gamma_2$}

   \node(4)(52,11){$F \gamma_1$}
   \node(5)(62,11){$F \gamma_2$}
   \put(50,8){\line(1,0){14}}
   \node(6)(57,5){$F \gamma_1\vee\gamma_2$}
  \end{picture}

  \begin{picture}(70,15)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \node(0)(12,11){$F \gamma_1$}
   \put(5,8){\line(1,0){14}}
   \node(1)(12,5){$V \gamma_1\rightarrow\gamma_2$}
   \put(0,8){\makebox(0,0){(4)}}

   \node(2)(32,11){$V \gamma_2$}
   \put(25,8){\line(1,0){14}}
   \node(3)(32,5){$V \gamma_1\rightarrow\gamma_2$}

   \node(4)(52,11){$V \gamma_1$}
   \node(5)(62,11){$F \gamma_2$}
   \put(50,8){\line(1,0){14}}
   \node(6)(57,5){$F \gamma_1\rightarrow\gamma_2$}
  \end{picture}

  \begin{picture}(70,15)(8,0)
   \gasset{Nw=20, Nh=6, Nmr=0, Nframe=n}

   \node(0)(7,11){$V \gamma_1$}
   \node(1)(17,11){$V \gamma_2$}
   \put(5,8){\line(1,0){14}}
   \put(0,8){\makebox(0,0){(5)}}
   \node(3)(12,5){$V \gamma_1\leftrightarrow\gamma_2$}

   \node(4)(27,11){$F \gamma_1$}
   \node(5)(37,11){$F \gamma_2$}
   \put(25,8){\line(1,0){14}}
   \node(6)(32,5){$V \gamma_1\leftrightarrow\gamma_2$}

   \node(7)(52,11){$V \gamma_1$}
   \node(8)(62,11){$F \gamma_2$}
   \put(50,8){\line(1,0){14}}
   \node(9)(57,5){$F \gamma_1\leftrightarrow\gamma_2$}

   \node(10)(72,11){$F \gamma_1$}
   \node(11)(82,11){$V \gamma_2$}
   \put(70,8){\line(1,0){14}}
   \node(12)(77,5){$F \gamma_1\leftrightarrow\gamma_2$}
  \end{picture}
 \end{center}

\end{document}
\endinput
\end
