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

\vspace*{3mm}
\begin{enumerate}
 \item 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$.

 \item 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}

 \item 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.)

 \item 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}

 \item 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$.

 \item 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$.)
\end{enumerate}

\newpage
\begin{flushleft} \bf\large
O algoritmo \textsf{satA-nd}:
\end{flushleft}

{\sf
\begin{tabbing}
 xxx\=xxx\=xxx\=xx\=xxxxxxxxxxxxx\=xxx\=xxx\=xxx\= \kill
 \> {\bf proc-nd} satA-nd(f\a'ormula $\gamma$): \\
 \> \> \textsl{conjunto de fórmulas marcadas} A; \\
 \> \> \textsl{conjunto de variáveis marcadas} $\Sigma$; \\
 \> \> \textsl{elemento de} $\{V,F\}$ s; \\
 \> \> $\Sigma=\emptyset$; \\
 \> \> $\mbox{A} := \{V\gamma\}$; \\
 \> \> {\bf repita} \\
 \> \> \> $s\gamma := \mbox{escolha}(A)$; $\mbox{A} := \mbox{A}-\{s\gamma\}$; \\
 \> \> \> {\bf caso} $s\gamma$ {\bf seja} \\
 \> \> \>  \> $*\mbox{variável}$: \> {\bf se} $\overline{\mbox{s}}\gamma\in\Sigma$ {\bf então}
                              {\em fracasso} {\bf senão} $\Sigma := \Sigma\cup \{s\gamma\}$ {\bf fimse} \\
 \> \> \>  \> $V\top$,$F\bot$: \> \{ continue \} \\
 \> \> \>  \> $V\bot$,$F\top$: \> {\em fracasso} \\
 \> \> \>  \> $V\neg\alpha$:
                   \> $\mbox{A} := \mbox{A}\cup \{F\alpha\}$ \\
 \> \> \>  \> $F\neg\alpha$:
                   \> $\mbox{A} := \mbox{A}\cup \{V\alpha\}$ \\
 \> \> \>  \> $V\alpha\wedge\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{V\alpha,V\beta\}$ \\
 \> \> \>  \> $F\alpha\wedge\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{\mbox{escolha-nd}(\{F\alpha,F\beta\})\}$
                                     $\{$ escolha não determin\a'{\i}stica $\}$\\
 \> \> \>  \> $V\alpha\vee\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{\mbox{escolha-nd}(\{V\alpha,V\beta\})\}$
                                     $\{$ escolha não determin\a'{\i}stica $\}$\\
 \> \> \>  \> $F\alpha\vee\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{F\alpha,F\beta\}$ \\
 \> \> \>  \> $V\alpha\rightarrow\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{\mbox{escolha-nd}(\{F\alpha,V\beta\})\}$
                                     $\{$ escolha não determin\a'{\i}stica $\}$\\
 \> \> \>  \> $F\alpha\rightarrow\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{V\alpha,F\beta\}$ \\
 \> \> \>  \> $V\alpha\leftrightarrow\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{\textit{escolha-nd}(\{\{V\alpha,V\beta\},\{F\alpha,F\beta\}\})\}$
                                     $\{$ escolha não determin\a'{\i}stica $\}$\\
 \> \> \>  \> $F\alpha\leftrightarrow\beta$:
                   \> $\mbox{A} := \mbox{A}\cup \{\textit{escolha-nd}(\{\{V\alpha,F\beta\},\{F\alpha,V\beta\}\})\}$
                                     $\{$ escolha não determin\a'{\i}stica $\}$\\
 \> \> \> {\bf fimcaso} \\
 \> \> {\bf até} $\mbox{A}=\emptyset$;\\
 \> \> {\em sucesso} \\
 \> {\bf fim} satA-nd \\
\end{tabbing}
}

\newpage
\begin{flushleft} \bf\large
As regras do sistema formal ${\cal S}_A$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrcrcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum e falsum}}\\
     \textsf{verp}: &                & \textsf{faln}: &  \\
                    &\overline{V\top}&                & \overline{F\bot} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
     \textsf{negp}: & F \alpha  & \textsf{negn}: &V \alpha \\
                    & \overline{V\neg\alpha}& & \overline{F \neg\alpha} \\
     \multicolumn{6}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & V\alpha \ \ V\beta           & \textsf{conjn1}: & F \alpha & \textsf{conjn2}: & F \beta \\
                     & \overline{V\alpha\wedge\beta}& & \overline{F \alpha\wedge\beta} & &\overline{F \alpha\wedge\beta} \\
     \multicolumn{6}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp1}: & V\alpha    & \textsf{disjp2}: & V \beta & \textsf{disjn}: & F \alpha\ \ F\beta \\
                     & \overline{V\alpha\vee\beta}& & \overline{V\alpha\vee\beta} & &\overline{F \alpha\vee\beta} \\
     \multicolumn{6}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp1}: & F\alpha    & \textsf{condp2}: & V \beta & \textsf{condn}: & V \alpha\ \ F\beta \\
                     & \overline{V\alpha\rightarrow\beta}& & \overline{V\alpha\rightarrow\beta} & &\overline{F \alpha\rightarrow\beta} \\
     \multicolumn{8}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp1}: & V\alpha\ \ V\beta & \textsf{bicp2}: & F\alpha\ \ F\beta & \textsf{bicn1}: & V \alpha\ \ F\beta & \textsf{bicn2}: & F \alpha\ \ V\beta \\
                     & \overline{V\alpha\leftrightarrow\beta}& & \overline{V\alpha\leftrightarrow\beta} & &\overline{F \alpha\leftrightarrow\beta}& &\overline{F \alpha\leftrightarrow\beta}
    \end{array}
  \]
 \end{center}

\vspace*{3mm}
\begin{flushleft} \bf\large
As regras do sistema formal ${\cal S}_B$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrcrcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum e falsum}}\\
     \textsf{verp}: &         & \textsf{faln}: &  \\
                   &\overline{\top}& & \overline{\neg\bot} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
      & & \textsf{negn}: &\alpha \\
      & & & \overline{\neg\neg\alpha} \\
     \multicolumn{6}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & \alpha \ \ \beta           & \textsf{conjn1}: &\neg\alpha & \textsf{conjn2}: &\neg\beta \\
                     & \overline{\alpha\wedge\beta}& & \overline{\neg(\alpha\wedge\beta)} & &\overline{\neg(\alpha\wedge\beta)} \\
     \multicolumn{6}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp1}: & \alpha    & \textsf{disjp2}: &\beta & \textsf{disjn}: & \neg\alpha\ \ \neg\beta \\
                     & \overline{\alpha\vee\beta}& & \overline{\alpha\vee\beta} & &\overline{\neg(\alpha\vee\beta)} \\
     \multicolumn{6}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp1}: & \neg\alpha    & \textsf{condp2}: &\beta & \textsf{condn}: &\alpha\ \ \neg\beta \\
                     & \overline{\alpha\rightarrow\beta}& & \overline{\alpha\rightarrow\beta} & &\overline{\neg(\alpha\rightarrow\beta)} \\
     \multicolumn{8}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp1}: & \alpha\ \ \beta & \textsf{bicp2}: & \neg\alpha\ \ \neg\beta & \textsf{bicn1}: &\alpha\ \ \neg\beta & \textsf{bicn2}: &\neg\alpha\ \ \beta \\
                     & \overline{\alpha\leftrightarrow\beta}& & \overline{\alpha\leftrightarrow\beta} & &\overline{\neg(\alpha\leftrightarrow\beta)}& &\overline{\neg(\alpha\leftrightarrow\beta)}
    \end{array}
  \]
 \end{center}

\newpage
\begin{flushleft} \bf\large
As regras lógicas do sistema formal ${\cal S}_C$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrcrcrc}
     \multicolumn{4}{l}{\textsf{Variáveis}} \\
     \textsf{varp}: & \Psi & \multicolumn{6}{l}{\mbox{se } \Psi \mbox{ é vazia ou contém apenas literais e não contém } \neg\nu}\\
                    & \overline{\Psi,\nu} \\
     \textsf{varn}: & \Psi & \multicolumn{6}{l}{\mbox{se } \Psi \mbox{ é vazia ou contém apenas literais e não contém } \nu}\\
                    & \overline{\Psi,\neg\nu} \\
     \multicolumn{4}{l}{\mbox{\sf Verum e falsum}}\\
     \textsf{verp}: & \Psi        & \textsf{faln}: & \Psi \\
                    &\overline{\Psi,\top}& & \overline{\Psi,\neg\bot} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
      & & \textsf{negn}: &\Psi,\alpha \\
      & & & \overline{\Psi,\neg\neg\alpha} \\
     \multicolumn{6}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & \Psi,\alpha,\beta           & \textsf{conjn1}: &\Psi,\neg\alpha & \textsf{conjn2}:
                      &\Psi,\neg\beta \\
                     & \overline{\Psi,\alpha\wedge\beta}& & \overline{\Psi,\neg(\alpha\wedge\beta)} &
                      &\overline{\Psi,\neg(\alpha\wedge\beta)} \\
     \multicolumn{6}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp1}: & \Psi,\alpha    & \textsf{disjp2}: &\Psi,\beta & \textsf{disjn}: & \Psi,\neg\alpha,\neg\beta \\
                     & \overline{\Psi,\alpha\vee\beta}& & \overline{\Psi,\alpha\vee\beta} &
                      &\overline{\Psi,\neg(\alpha\vee\beta)} \\
     \multicolumn{6}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp1}: & \Psi,\neg\alpha    & \textsf{condp2}: &\Psi,\beta & \textsf{condn}: &\Psi,\alpha,\neg\beta \\
                     & \overline{\Psi,\alpha\rightarrow\beta}& & \overline{\Psi,\alpha\rightarrow\beta} &
                      &\overline{\Psi,\neg(\alpha\rightarrow\beta)} \\
     \multicolumn{8}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp1}: & \Psi,\alpha,\beta & \textsf{bicp2}: & \Psi,\neg\alpha,\neg\beta & \textsf{bicn1}:
                      & \Psi,\alpha,\neg\beta & \textsf{bicn2}: &\Psi,\neg\alpha,\beta \\
                     & \overline{\Psi,\alpha\leftrightarrow\beta}& & \overline{\Psi,\alpha\leftrightarrow\beta}
                      & &\overline{\Psi,\neg(\alpha\leftrightarrow\beta)}
                      & &\overline{\Psi,\neg(\alpha\leftrightarrow\beta)}
    \end{array}
  \]
 \end{center}

\newpage
\begin{flushleft} \bf\large
As regras lógicas do sistema formal ${\cal S}_I$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum} \mbox{ e } \mbox{\sf falsum}}\\
     \textsf{falp}: &  & \textsf{vern}: &  \\
                    & \overline{\Psi,\bot} & & \overline{\Psi,\neg\top} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
      & & \textsf{negn}: & \Psi,\alpha \\
      & &                  & \overline{\Psi,\neg\neg\alpha} \\
     \multicolumn{4}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & \Psi,\alpha,\beta & \textsf{conjn}: &\Psi,\neg\alpha\ \ \ \Psi,\neg\beta \\
                     & \overline{\Psi,\alpha\wedge\beta}& & \overline{\ \ \Psi,\neg(\alpha\wedge\beta\ \ )} \\
     \multicolumn{4}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp}: & \Psi,\alpha\ \ \ \Psi,\beta & \textsf{disjn}: &\Psi,\neg\alpha,\neg\beta \\
                     & \overline{\ \ \Psi,\alpha\vee\beta\ \ }& & \overline{\Psi,\neg(\alpha\vee\beta)} \\
     \multicolumn{4}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp}: & \Psi,\neg\alpha\ \ \ \Psi,\beta & \textsf{condn}: &\Psi,\alpha,\neg\beta \\
                     & \overline{\ \ \ \Psi,\alpha\rightarrow\beta\ \ \ }& & \overline{\Psi,\neg(\alpha\rightarrow\beta)} \\
     \multicolumn{4}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp}: & \Psi,\alpha,\beta\ \ \Psi,\neg\alpha,\neg\beta & \textsf{bicn}: &\Psi,\alpha,\neg\beta\ \ \Psi,\neg\alpha,\beta \\
                    & \overline{\ \ \ \ \ \ \Psi,\alpha\leftrightarrow\beta\ \ \ \ \ \ }& & \overline{\ \ \  \Psi,\neg(\alpha\leftrightarrow\beta)\ \ \ }
    \end{array}
  \]
 \end{center}

\vspace*{3mm}
\begin{flushleft} \bf\large
As regras lógicas do sistema formal ${\cal S}_T$:
\end{flushleft}

 \begin{center}
  \[\begin{array}{rcrc}
     \multicolumn{4}{l}{\mbox{\sf Verum} \mbox{ e } \mbox{\sf falsum}}\\
     \textsf{verp}: &                      & \textsf{faln}: &  \\
                    & \overline{\Psi,\top} &                &  \overline{\Psi,\neg\bot} \\
     \multicolumn{4}{l}{\mbox{\sf Nega\c{c}ão}} \\
      & & \textsf{negn}: & \Psi,\alpha \\
      & &                  & \overline{\Psi,\neg\neg\alpha} \\
     \multicolumn{4}{l}{\mbox{\sf Conjunção}} \\
     \textsf{conjp}: & \Psi,\alpha\ \ \ \Psi,\beta & \textsf{conjn}: &\Psi,\neg\alpha,\neg\beta \\
                     & \overline{\ \Psi,\alpha\wedge\beta\ }& & \overline{\ \ \Psi,\neg(\alpha\wedge\beta)\ \ } \\
     \multicolumn{4}{l}{\mbox{\sf Disjunção}} \\
     \textsf{disjp}: & \Psi,\alpha,\beta & \textsf{disjn}: &\Psi,\neg\alpha\ \ \ \Psi,\neg\beta \\
                     & \overline{\Psi,\alpha\vee\beta}& & \overline{\ \ \ \Psi,\neg(\alpha\vee\beta)\ \ \ } \\
     \multicolumn{4}{l}{\mbox{\sf Condicional}} \\
     \textsf{condp}: & \Psi,\neg\alpha,\beta & \textsf{condn}: &\Psi,\alpha\ \ \ \Psi,\neg\beta \\
                     & \overline{\ \Psi,\alpha\rightarrow\beta\ }& & \overline{\ \ \Psi,\neg(\alpha\rightarrow\beta)\ \ } \\
     \multicolumn{4}{l}{\mbox{\sf Bicondicional}} \\
     \textsf{bicp}: & \Psi,\neg\alpha,\beta\ \ \Psi,\alpha,\neg\beta & \textsf{bicn}: &\Psi,\alpha,\beta\ \ \Psi,\neg\alpha,\neg\beta \\
                    & \overline{\ \ \ \ \ \ \Psi,\alpha\leftrightarrow\beta\ \ \ \ \ \ }& & \overline{\ \ \  \Psi,\neg(\alpha\leftrightarrow\beta)\ \ \ }
    \end{array}
  \]
 \end{center}

\end{document}
