\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 Primeira Prova}/Solução do professor

\vspace*{3mm}
\begin{enumerate}
 \item {\footnotesize Escreva fórmulas $\gamma$ tais que $\gamma \equiv \alpha\leftrightarrow\beta$ e que satisfaçam as seguintes
       restrições:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\gamma$ é uma conjunção de disjunções.
				
        \item $\gamma$ é uma disjunção de conjunções.
       \end{list}
			 Para cada caso, mostre que, realmente, $\gamma \equiv \alpha\leftrightarrow\beta$.}

       \emph{Solução}:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\gamma=(\neg\alpha\vee\beta)\wedge(\alpha\vee\neg\beta)$. Pela tabela da verdade:
				      \begin{center}
               \begin{tabular}{cc|c|c|c|c|c|c|}
                $\alpha$ & $\beta$ & $\neg\alpha$ & $\neg\beta$ & $\neg\alpha\vee\beta$ & $\alpha\vee\neg\beta$ &
								$(\neg\alpha\vee\beta)\wedge(\alpha\vee\neg\beta)$ & $\alpha\leftrightarrow\beta$\\ \hline
                V & V & F & F & V & V & V & V\\ 
                V & F & F & V & F & V & F & F\\ 
                F & V & V & F & V & F & F & F\\ 
                F & F & V & V & V & V & V & V\\ 
               \end{tabular}
              \end{center}
 
        \item $\gamma=(\alpha\wedge\beta)\vee(\neg\alpha\wedge\neg\beta)$. Pela tabela da verdade:
				      \begin{center}
               \begin{tabular}{cc|c|c|c|c|c|c|}
                $\alpha$ & $\beta$ & $\neg\alpha$ & $\neg\beta$ & $\alpha\wedge\beta$ & $\neg\alpha\wedge\neg\beta$ &
								$(\alpha\wedge\beta)\vee(\neg\alpha\wedge\neg\beta)$ & $\alpha\leftrightarrow\beta$\\ \hline
                V & V & F & F & V & F & V & V\\ 
                V & F & F & V & F & F & F & F\\ 
                F & V & V & F & F & F & F & F\\ 
                F & F & V & V & F & V & V & V\\ 
               \end{tabular}
              \end{center}
       \end{list}
 \item {\footnotesize Defina usando $v^i$:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Modelo para um conjunto de fórmulas.
        \item Conjunto de fórmulas insatisfatível.
       \end{list}}

       \emph{Solução}:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $i$ é um modelo para $H$ sse $v^i(\alpha)=V$ para toda $\alpha\in H$.
        \item $H$ é insatisfatível sse para toda $i$ $v^i(\alpha)=F$ para alguma $\alpha\in H$.
       \end{list}


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

       \emph{Solução}:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\alpha$ é falseável sse $\neg\alpha$ é satisfatível.
        \item $\alpha$ é tautologia sse $\neg\alpha$ não é satisfatível.
				\item $\alpha$ é contradição sse $\alpha$ não é satisfatível.
       \end{list}

 \item {\footnotesize Seja $\alpha=(\neg p\rightarrow q)\wedge\neg q$.
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Apresente uma árvore de computação para a chamada $\textsf{satA-nd}(\alpha)$.
        \item Construa uma derivação de $\alpha$ nos sistemas formais ${\cal S}_A$, ${\cal S}_B$ e ${\cal S}_C$, 
				      mostrando que $\alpha$ é satisfatível.
       \end{list}}

       \emph{Solução}:
        \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Árvore de computação para $\textsf{satA-nd}(\alpha)$:
				
              \begin{picture}(40,92)(-30,0)
               \put(20,88){\makebox(0,0){$\emptyset\{V(\neg p\rightarrow q)\wedge\neg q\}$}}
               \put(20,85){\line(0,-1){8}}
               \put(21,81){\makebox(0,0)[l]{\sf conjp}}

               \put(20,74){\makebox(0,0){$\emptyset\{V\neg p\rightarrow q, \underline{V\neg q}\}$}}
               \put(20,71){\line(0,-1){8}}
               \put(21,67){\makebox(0,0)[l]{\sf negp}}

               \put(20,60){\makebox(0,0){$\emptyset\{V\neg p\rightarrow q,Fq\}$}}
               \put(20,57){\line(0,-1){8}}
               \put(21,53){\makebox(0,0)[l]{$\Sigma$}}
               \put(20,46){\makebox(0,0){$\{Fp\}\{V\neg p\rightarrow p\}$}}

               \put(20,43){\line(-1,-1){8}}
               \put(14,39){\makebox(0,0)[r]{\sf condp1}}
               \put(20,43){\line(1,-1){8}}
               \put(26,39){\makebox(0,0)[l]{\sf condp2}}
	
               \put(5,32){\makebox(0,0){$\{Fp\}\{F\neg p\}$}}
               \put(35,32){\makebox(0,0){$\{Fq\}\{Vq\}$}}
               \put(35,28){\makebox(0,0){\textit{fracasso}}}

               \put(5,29){\line(0,-1){8}}
               \put(6,25){\makebox(0,0)[l]{\sf negn}}
               \put(5,18){\makebox(0,0){$\{Fq\}\{Vp\}$}}
               \put(5,15){\line(0,-1){8}}
               \put(6,11){\makebox(0,0)[l]{$\Sigma$}}
               \put(5,4){\makebox(0,0){$\{Fq,Vp\}\emptyset$}}
               \put(5,0){\makebox(0,0){\textit{sucesso}}}
              \end{picture}

        \item Derivação de $\alpha$ em ${\cal S}_A$:
              \begin{tabbing}
               xxx\= 4. \=$V(\neg p\rightarrow q)\wedge\neg q$ \ \ \ \= \kill
                  \> 1. \>$V p$                                \> ($\Sigma$)\\
                  \> 2. \>$F \neg p$                           \> (\textsf{negn} 1) \\
                  \> 3. \>$V\neg p\rightarrow q$               \> (\textsf{condp1} 2) \\
                  \> 4. \>$F q$                                \> ($\Sigma$)\\
                  \> 5. \>$V\neg q$                            \> (\textsf{negp} 4) \\
                  \> 6. \=$V(\neg p\rightarrow q)\wedge\neg q$ \> (\textsf{conjp} 3,5)
              \end{tabbing}
							Derivação de $\alpha$ em ${\cal S}_B$:
              \begin{tabbing}
               xxx\= 4. \=$(\neg p\rightarrow q)\wedge\neg q$ \ \ \ \= \kill
                  \> 1. \>$p$                                 \> ($\Sigma$)\\
                  \> 2. \>$\neg\neg p$                        \> (\textsf{negn} 1) \\
                  \> 3. \>$\neg p\rightarrow q$               \> (\textsf{condp1} 2) \\
                  \> 4. \>$\neg q$                            \> ($\Sigma$)\\
                  \> 5. \=$(\neg p\rightarrow q)\wedge\neg q$ \> (\textsf{conjp} 3,5)
              \end{tabbing}
							Derivação de $\alpha$ em ${\cal S}_C$:
              \begin{tabbing}
               xxx\= 4. \=$(\neg p\rightarrow q)\wedge\neg q$ \ \ \ \= \kill
							    \> 1. \>$\lambda$                             \> (\textsf{Ax}) \\
                  \> 2. \>$p$                                   \> (\textsf{varp})\\
                  \> 3. \>$p,\neg q$                            \> (\textsf{varn}) \\
                  \> 4. \>$\neg \neg p,\neg q$                  \> (\textsf{negn}) \\
                  \> 5. \>$\neg p\rightarrow q,\neg q$          \> (\textsf{condp1}) \\
                  \> 6. \>$(\neg p\rightarrow q)\wedge\neg q$   \> (\textsf{conjp})
              \end{tabbing}

       \end{list}

 \item {\footnotesize Seja $\alpha=((p\rightarrow q)\rightarrow p)\leftrightarrow p$.
       Apresente uma derivação de $\alpha$ no sistema formal ${\cal S}_T$, ou então uma derivação de $\neg\alpha$
			 no sistema formal ${\cal S}_I$.}

       \emph{Solução}:

							Derivação de $\alpha$ em ${\cal S}_T$:
              \begin{tabbing}
               xxx\= 4. \=$((p\rightarrow q)\rightarrow p)\leftrightarrow p$ \ \ \ \= \kill
							    \> 1. \>$\neg p,q,p$                                       \> (\textsf{Ax}) \\
                  \> 2. \>$p\rightarrow q,p$                                 \> (\textsf{condp1})\\
                  \> 3. \>$\neg p,p$                                         \> (\textsf{Ax}) \\
                  \> 4. \>$\neg((p\rightarrow q)\rightarrow p),p$            \> (\textsf{condn} 2,3) \\
                  \> 5. \>$\neg(p\rightarrow q),p,\neg p$                    \> (\textsf{Ax}) \\
                  \> 6. \>$(p\rightarrow q)\rightarrow p,\neg p$             \> (\textsf{condp} 5) \\
                  \> 7. \>$((p\rightarrow q)\rightarrow p)\leftrightarrow p$ \> (\textsf{bicp} 4,6)
              \end{tabbing}

 \item {\footnotesize Como os sistemas formais ${\cal S}_I$ e ${\cal S}_T$ podem ser usados para, dados $H\subseteq {\cal F}$ e
       $\alpha\in{\cal F}$, provar que $H\models\alpha$? (Deve-se dizer apenas o que são $X$ e $Y$ em: $H\models\alpha$
			 sse $X \vdash Y$ no sistema ${\cal S}_I$. Analogamente para ${\cal S}_T$.)}

       \emph{Solução}:
 
       Seja $\textsf{seq}(X)$ uma sequência das fórmulas no conjunto de fórmulas $X$. Então:
			\begin{itemize}
			 \item $H\models\alpha$ sse $\emptyset\vdash\textsf{seq}(H\cup\{\neg\alpha\})$ em ${\cal S}_I$.
			 \item $H\models\alpha$ sse $\emptyset\vdash\textsf{seq}(\{\neg\gamma|\gamma\in H\}\cup\{\alpha\})$ em ${\cal S}_T$.
			\end{itemize}
\end{enumerate}

\end{document}
