\documentclass[12pt, a4paper]{report}

\usepackage[portuguese]{babel}
\usepackage{fullpage}

\newcounter{conta}

\begin{document}
 
\noindent {\it TECC: L\'ogica Aplicada a Computa\c c\~ao}
\hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2003 \\
\noindent Professor: Newton Jos\'{e} Vieira \hfill DCC/ICEx/UFMG \\
\noindent {\bf Lista de exerc\'{\i}cios preparat\'oria para a Primeira Prova}

\begin{enumerate}
 \item Para cada uma das seguintes f\'ormulas:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $p\wedge(r\uparrow q)\vee r\wedge s$
        \item $(p\downarrow q)\vee(r\downarrow s)\vee((r\leftrightarrow s)
               \wedge(p\uparrow q))$
        \item $\neg(p\leftrightarrow r)\rightarrow((p\leftrightarrow q)
               \rightarrow\neg (q\leftrightarrow r))$
       \end{list}
       fa\c ca:
       \begin{itemize}
        \item Construa sua tabela da verdade.
        \item Diga se \'e tautol\'ogica, insatisfat\'{\i}vel ou
              contingente.
        \item Construa uma f\'ormula logicamente equivalente na forma normal
              conjuntiva.
       \end{itemize}

 \item Sem usar tabela da verdade, mostre as seguintes equival\^encias:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $A\vee(A\wedge(\neg A\vee B))\vee B\equiv A\vee B$.
        \item $(A\wedge \neg B)\vee(\neg A\wedge B)\equiv \neg(A\wedge B)\wedge
               (A\vee B)$.
        \item $A\leftrightarrow B\equiv(\neg A\vee\neg B)\vee(\neg A\wedge\neg B)$.
        \item $\neg(A\leftrightarrow B)\equiv\neg A\leftrightarrow B$.
        \item $(A\wedge B)\rightarrow C \equiv (A\wedge\neg C)\rightarrow\neg B$.
       \end{list}

 \item Defina (se possivel) todos os operadores booleanos utilizando apenas
       $\neg$ e $\leftrightarrow$.

 \item Mostre que para todas as f\'ormulas do c\'alculo proposicional $A$ e $B$:
       \[A\equiv B \mbox{ se, e somente se, }\models A\leftrightarrow B\mbox{.}\]

 \item Como usar tableaux sem\^anticos para mostrar:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item Que uma f\'ormula \'e satisfat\'{\i}vel?
        \item Que uma f\'ormula \'e false\'avel?
        \item Que uma f\'ormula \'e insatisfat\'{\i}vel?
        \item Que uma f\'ormula \'e v\'alida?
        \item Que uma f\'ormula \'e contingente?
        \item Que $\Sigma\models A$, onde $\Sigma$ \'e um conjunto de f\'ormulas
              e $A$ \'e uma f\'ormula?
        \item Que $A\equiv B$?
       \end{list}

 \item Utilize tableaux sem\^anticos para mostrar:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $(p\vee q)\wedge(\neg p\vee q)\wedge(p\vee \neg q)\wedge\neg(p\wedge q)$
              \'e insatisfat\'{\i}vel.
        \item $\{p\vee q\vee r, p\rightarrow s, \neg s\rightarrow \neg q,r\leftrightarrow s\}
               \models s$.
       \end{list}

 \item Prove no sistema de Gentzen que:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
         \item $\vdash ((A\rightarrow B)\rightarrow A)\rightarrow A$.
         \item $\vdash ((A\wedge B)\rightarrow C \wedge (A\wedge\neg C))\rightarrow\neg B$.
       \end{list}

 \item Usando resolu\c c\~ao, mostre que:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\{(p\wedge q)\rightarrow v,\neg s,\neg p\rightarrow s,\neg s\rightarrow r,
                 r\rightarrow q\}\models v$.
        \item $\{v\rightarrow p,(\neg v\wedge q)\rightarrow s\}\models \neg p\rightarrow(q\rightarrow s)$.
        \item $\{p\rightarrow r,r\rightarrow s,s\rightarrow\neg q\}\models \neg (p\wedge q)$.
       \end{list}

 \item Construa BDDs para as seguintes f\'ormulas:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $((p\vee q)\leftrightarrow(r\wedge s))\downarrow (p\uparrow (q\rightarrow r))$.
        \item $(p\vee (p\downarrow q)\wedge (r\rightarrow p))\rightarrow((p\oplus q)
               \leftrightarrow \neg(p\wedge r))$.
       \end{list}

 %==============

 \item Prove as seguintes equival\^encias l\'ogicas usando BDDs:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $(p\vee q)\wedge (\neg p\wedge \neg q)\equiv \bot$.
        \item $\neg (\neg (p\vee q)\vee \neg(p\vee r))\equiv p \vee (q\wedge r)$.
       \end{list}

 \item As f\'ormulas $\forall y\exists x\, p(x,y)$ e $\exists x \forall y\, p(x,y)$ s\~ao
       equivalentes? Justifique sua resposta.

 \item Prove a validade das seguintes f\'ormulas usando tableaux:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\forall x (A(x)\vee B(x))\rightarrow (\forall x A(x)\vee \exists x B(x))$.
        \item $\forall x (A(x)\rightarrow B(x))\rightarrow (\exists x A(x)\rightarrow \exists x B(x))$.
       \end{list}

\end{enumerate}

\end{document}
