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

\vspace*{3mm}
\begin{enumerate}
 \item Seja $\gamma=(p\wedge((\neg q\wedge s)\vee r))\vee(q\wedge(\neg r\vee\neg s))$. Obtenha uma fórmula
       $\gamma'$ na FNC usando o método visto em aula (e na apostila) que produz, em tempo linear, a partir de uma
       fórmula $\gamma$ na FNN, uma fórmula $\gamma'$ na FNC tal que $\gamma'$ é satisfatível se, e somente se,
       $\gamma$ é satisfatível. Lembrete: o método cria uma variável nova para cada subfórmula que não seja literal.
 \item Suponha que voc\^e tenha algoritmos para determinar, para uma f\'ormula
       qualquer, se ela \'e:
       \begin{list}{\alph{conta})}{\usecounter{conta}}
        \item tautologia;
        \item contradi\c c\~ao;
        \item satisfat\'{\i}vel;
        \item false\'avel.
       \end{list}
       Explique como voc\^e poderia utilizar cada um desses quatro algoritmos
       para determinar, dados um conjunto finito de f\'ormulas $H$ e uma f\'ormula
       $\alpha$, se $H\models \alpha$.
 \item Mostre que a seguinte fórmula é válida: $\exists x(D(x)\rightarrow \forall x D(x))$. Interpretando $D(x)$
       como $x$ \textit{dança} e supondo o universo como constituído de pessoas, ela diz ``existe alguém tal que, se
       ele dança, então todos dançam''.
 \item Apresente uma dedu\c{c}\~ao no sistema de dedu\c{c}\~ao natural que demonstre que
        $$\{\forall x(p(x)\rightarrow q(x)),\exists x\,p(x)\}\models \exists x\,q(x)\mbox{.}$$
 \item Determine umgs (caso existam) para as seguintes express\~{o}es:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $p(x,x,g(x))$ e $p(y,f(z),z)$
        \item $p(x,x,g(x))$ e $p(y,f(z),w)$
       \end{list}
 \item Encontre um conjunto de cl\'{a}usulas para cada uma das senten\c{c}as:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\neg (\forall x\,p(x) \rightarrow \neg\exists y\forall x\, q(y,x))$
        \item $\forall x \{\neg p(x,0) \rightarrow [\exists y\, p(y,f(x))\wedge\forall z(p(z,f(x))\rightarrow p(y,z))]\}$
       \end{list}
\end{enumerate}

\vspace*{3mm}
\hrule
\vspace*{.5mm}
\hrule
\vfill
 No verso estão exemplificadas regras do sistema de dedução natural.
\vfill
\newpage
\textbf{Algumas regras do sistema de dedução natural}:
\begin{itemize}
 \item Conectivo $\wedge$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (I$\wedge$):
              \begin{center}
               \begin{tabular}{c}
               $\alpha$\hspace*{3mm}$\beta$ \\ \cline{1-1}
               $\alpha\wedge\beta$
               \end{tabular}
              \end{center}
        \item Elimina\c{c}\~ao (E$\wedge_1$ e E$\wedge_2$):
              \begin{center}
               \begin{tabular}{ccc}
                $\alpha\wedge\beta$ &\hspace*{10mm} & $\alpha\wedge\beta$\\ \cline{1-1}\cline{3-3}
                $\alpha$            &               & $\beta$
               \end{tabular}
              \end{center}
       \end{itemize}
 \item Conectivo $\rightarrow$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (I$\rightarrow$):
              \begin{center}
               \fbox{\parbox[t]{.3cm}{\hspace*{.5mm}$\alpha$\\ \hspace*{1mm}$\vdots$\\ \hspace*{.4mm}$\beta$}} \\
               \rule{1cm}{0.2mm} \\
               $\alpha\rightarrow\beta$
              \end{center}
        \item Elimina\c{c}\~ao (E$\rightarrow$):
              \begin{center}
               \begin{tabular}{c}
               $\alpha$\hspace*{3mm}$\alpha\rightarrow\beta$ \\ \cline{1-1}
               $\beta$
               \end{tabular}
              \end{center}
       \end{itemize}
 \item Conectivo $\forall$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (I$\forall$):
              \begin{center}
               \fbox{\parbox[t]{.9cm}{\hspace*{.5mm}$\nu_0$\\ \hspace*{5mm}$\vdots$\\ \hspace*{3.4mm}$\alpha_{\nu}^{\nu_0}$}} \\
               \rule{1.2cm}{0.2mm} \\
               $\forall \nu\alpha$
              \end{center}
        \item Elimina\c{c}\~ao (E$\forall$):
              \begin{center}
               \begin{tabular}{c}
               $\forall \nu\alpha$ \\ \cline{1-1}
               $\alpha_{\nu}^t$
               \end{tabular}
              \end{center}
       \end{itemize}
 \item Conectivo $\exists$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (I$\exists$):
              \begin{center}
               \begin{tabular}{c}
               $\alpha_{\nu}^t$ \\ \cline{1-1}
               $\exists \nu\,\alpha$
               \end{tabular}
              \end{center}
        \item Elimina\c{c}\~ao (E$\exists$):
              \begin{center}
               $\exists \nu\,\alpha$\hspace*{3mm}\fbox{\parbox[b]{11.4mm}{\hspace*{.5mm}$\nu_0 \;\;\alpha_{\nu}^{\nu_0}$\\
                \hspace*{7mm}$\vdots$\\
                \hspace*{6mm}$\beta$}} \\
               \rule{3cm}{0.2mm} \\
               $\beta$
              \end{center}
       \end{itemize}
\end{itemize}


\end{document}
