\documentclass[12pt, a4paper]{report}

\pagestyle{empty}
\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 Primeiro TP} \hfill Entrega: 30/10/03

\vspace*{5mm}
Implemente, em sua linguagem de programa\c c\~ao preferida, um sistema de infer\^encia
para o c\'alculo proposicional baseado em {\em tableaux\/} sem\^anticos. O programa
dever\'a receber como entrada uma f\'ormula do c\'alculo proposicional e determinar
se a mesma \'e satisfat\'{\i}vel ou n\~ao. Para uma f\'ormula satisfat\'{\i}vel o
programa dever\'a produzir explicitamente a interpreta\c c\~ao encontrada que satisfaz
a f\'ormula. Para teste do programa, utilize o mesmo
para resolver as quest\~oes 3, 5 e 6 da primeira lista de exerc\'{\i}cios, transcritas
abaixo:
\begin{enumerate}

 \item[3.] Prove as seguintes equival\^encias l\'ogicas:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $A\wedge(B\vee C)\equiv (A\wedge B)\vee(A \wedge C)$.
        \item $A\rightarrow B\equiv \neg A \vee B$.
        \item $A\rightarrow B\equiv \neg (A \wedge \neg B)$.
        \item $((A\oplus B)\oplus B)\equiv A$.
       \end{list}

 \item[5.] Verifique, dentre as seguintes f\'ormulas, quais s\~ao v\'alidas, quais
       s\~ao insatisfat\'{\i}veis e quais s\~ao contingentes (satisfat\'{\i}veis
       e false\'aveis):
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $p\wedge q\wedge(\neg p\vee\neg q)$.
        \item $(p\rightarrow q)\rightarrow (q\rightarrow p)$.
        \item $(p\rightarrow q)\rightarrow (\neg p\rightarrow \neg q)$.
        \item $(p\rightarrow q)\rightarrow (\neg q\rightarrow \neg p)$.
        \item $(p\leftrightarrow q)\rightarrow (\neg p\leftrightarrow \neg q)$.
        \item $(p\rightarrow(r\wedge q))\rightarrow(\neg r\rightarrow(p\vee r))$.
        \item $(p\wedge q)\rightarrow((p\rightarrow r)\rightarrow((r\rightarrow p)
               \rightarrow (p\leftrightarrow q)))$.
       \end{list}

 \item[6.] Verifique a validade (ou n\~ao) das seguintes consequ\^encias l\'ogicas:
       \begin{list}{(\alph{conta})}{\usecounter{conta}}
        \item $\{p\rightarrow q, r\rightarrow q\} \models p\rightarrow r$.
        \item $\{p\wedge q, q\wedge r\} \models p\rightarrow r$.
        \item $\{p\rightarrow q, p\rightarrow r\} \models p\vee q\vee r$.
       \end{list}

\end{enumerate}
\end{document}
