\documentclass[12pt,a4paper]{report}

\pagestyle{empty}
\begin{document} \large

\noindent {\bf\Large Os $2^{2^2}$ operadores booleanos de 2 argumentos:}

\vspace*{1.5cm}
\begin{tabular}{|c|c||c|c|c|c|c|c|c|c|} \hline
$x_1$ & $x_2$ & $o_1$ & $o_2$ & $o_3$ & $o_4$ & $o_5$ & $o_6$ & $o_7$ & $o_8$ \\ \hline\hline
  V & V & V & V & V & V & V & V & V & V \\ \hline
  V & F & V & V & V & V & F & F & F & F \\ \hline
  F & V & V & V & F & F & V & V & F & F \\ \hline
  F & F & V & F & V & F & V & F & V & F \\ \hline
\multicolumn{10}{l}{\ } \\
\multicolumn{10}{l}{\ } \\ \hline
$x_1$ & $x_2$ & $o_9$ & $o_{10}$ & $o_{11}$ & $o_{12}$ & $o_{13}$ & $o_{14}$ & $o_{15}$ & $o_{16}$ \\ \hline\hline
  F & F & F & F & F & F & F & F & F & F \\ \hline
  V & F & V & V & V & V & F & F & F & F \\ \hline
  F & V & V & V & F & F & V & V & F & F \\ \hline
  F & F & V & F & V & F & V & F & V & F \\ \hline
\end{tabular}

\vspace*{1.5cm}
\noindent {\bf\Large Os operadores importantes e suas nega\c c\~oes:}

\vspace*{1.5cm}
\begin{tabular}{|l|l|c||l|l|c|} \hline
 op & nome & s\'{\i}mbolo & op & nome & s\'{\i}mbolo \\ \hline\hline
 $o_2$ & disjun\c c\~ao & $\vee$ & $o_{15}$ & nou & $\downarrow$ \\ \hline
 $o_3$ & implica\c c\~ao rec\'{\i}proca & $\leftarrow$ & $o_{14}$ & & \\ \hline
 $o_5$ & implica\c c\~ao & $\rightarrow$ & $o_{12}$ & & \\ \hline
 $o_7$ & equival\^encia & $\leftrightarrow$ & $o_{10}$ & ou exclusivo & $\oplus$ \\ \hline
 $o_8$ & conjun\c c\~ao & $\wedge$ & $o_9$ & ne & $\uparrow$ \\ \hline
\end{tabular}

\pagebreak

\noindent {\bf\Large Nota\c c\~ao:}

\vspace*{1.5cm}
\begin{tabular}{|c|c|c|} \hline
 Operador      & Alternativas          & Linguagem C \\ \hline\hline
 $\neg$        & $\sim$                & $!$ \\ \hline
 $\wedge$      & $\&$                  & $\&$ \\ \hline
 $\vee$        &                       & $|$ \\ \hline
 $\rightarrow$ & $\supset,\Rightarrow$ & \\ \hline
 $\leftrightarrow$ & $\equiv,\Leftrightarrow$ & \\ \hline
 $\oplus$          & $\not\equiv$      & $\hat{\ }$ \\ \hline
 $\uparrow$        & $|$               & \\ \hline
\end{tabular}

\vspace*{2cm}
\noindent {\bf\Large Defini\c c\~ao de f\'ormula:}

\vspace*{1.5cm}
Uma {\em f\'ormula\/} \'e uma palavra que pode ser derivada a partir da
gram\'atica:

\vspace*{.5cm}
\begin{tabbing}
\hspace*{1cm}\ \=xxx\=xxxxxxxxxxxxxxxxxxxxxxx\= \kill
               \>1. \>{\em fml\/} $\;\;::=\;\;$ $p$ \> para qualquer $p\in {\cal P}$ \\
               \>2. \>{\em fml\/} $\;\;::=\;\;$ $\neg$ {\em fml\/} \\
               \>3. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\vee$ {\em fml\/} \\
               \>4. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\wedge$ {\em fml\/} \\
               \>5. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\rightarrow$ {\em fml\/} \\
               \>6. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\leftrightarrow$ {\em fml\/} \\
               \>7. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\oplus$ {\em fml\/} \\
               \>8. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\uparrow$ {\em fml\/} \\
               \>9. \>{\em fml\/} $\;\;::=\;\;$ {\em fml\/} $\downarrow$ {\em fml\/} \\
\end{tabbing}

\pagebreak

\noindent {\bf\Large Indu\c c\~ao estrutural:}

\vspace*{1cm}
Para mostrar $\mbox{\em prop\/}(A)$ para toda f\'ormula $A\in {\cal F}$, \'e suficiente mostrar:

\vspace*{.5cm}
\begin{enumerate}
 \item $\mbox{\em prop\/}(p)$ vale para todo \'atomo $p$.
 \item Supondo $\mbox{\em prop\/}(A)$, ent\~ao $\mbox{\em prop\/}(\neg A)$ vale.
 \item Supondo $\mbox{\em prop\/}(A_1)$ e $\mbox{\em prop\/}(A_2)$,
       ent\~ao $\mbox{\em prop\/}(A_1 \;\mbox{\em op}\; A_2)$ vale, para cada operador {\em op}.
\end{enumerate}

\vspace*{1.5cm}
\noindent {\bf\Large Avalia\c c\~ao de valores de f\'ormulas:}

\vspace*{.5cm}
\begin{tabular}{|c|c|c|c|} \hline
 $A$ & $\nu(A_1)$ & $\nu(A_2)$  & $\nu(A)$  \\ \hline\hline
 $\neg A_1$ & V &    & F  \\ \hline
 $\neg A_1$ & F &    & V  \\ \hline
 $A_1 \vee A_2$ & F & F & F  \\ \hline
 $A_1 \vee A_2$ & \multicolumn{2}{|c|}{caso contr\'ario} & V  \\ \hline
 $A_1 \wedge A_2$ & V & V & V  \\ \hline
 $A_1 \wedge A_2$ & \multicolumn{2}{|c|}{caso contr\'ario} & F  \\ \hline
 $A_1 \rightarrow A_2$ & V & F & F  \\ \hline
 $A_1 \rightarrow A_2$ & \multicolumn{2}{|c|}{caso contr\'ario} & V  \\ \hline\hline
 $A_1 \uparrow A_2$ & V & V & F  \\ \hline
 $A_1 \uparrow A_2$ & \multicolumn{2}{|c|}{caso contr\'ario} & V  \\ \hline
 $A_1 \downarrow A_2$ & F & F & V  \\ \hline
 $A_1 \downarrow A_2$ & \multicolumn{2}{|c|}{caso contr\'ario} & F  \\ \hline
 $A_1 \leftrightarrow A_2$ & \multicolumn{2}{|c|}{$\nu(A_1)=\nu(A_2)$} & V  \\ \hline
 $A_1 \leftrightarrow A_2$ & \multicolumn{2}{|c|}{$\nu(A_1)\not=\nu(A_2)$} & F  \\ \hline
 $A_1 \oplus A_2$ & \multicolumn{2}{|c|}{$\nu(A_1)\not=\nu(A_2)$} & V  \\ \hline
 $A_1 \oplus A_2$ & \multicolumn{2}{|c|}{$\nu(A_1)=\nu(A_2)$} & F  \\ \hline
\end{tabular}

\pagebreak

\noindent {\bf\Large Equival\^encias l\'ogicas:}

\vspace*{.5cm}
\begin{tabular}{ll} 
 $A\vee\top \equiv \top$ & $A\wedge\top \equiv A$ \\
 $A\vee\bot \equiv A$ & $A\wedge\bot \equiv \bot$ \\
 $A\rightarrow\top \equiv \top$ & $\top\rightarrow A \equiv A$ \\
 $A\rightarrow\bot \equiv \neg A$ & $\bot\rightarrow A \equiv \top$ \\
 $A\leftrightarrow\top \equiv A$ & $A\oplus\top \equiv \neg A$ \\
 $A\leftrightarrow\bot \equiv \neg A$ & $A\oplus\bot \equiv A$ \\
 \\
 $A \equiv \neg\neg A$ \\
 $A \equiv A\wedge A$ & $A \equiv A\vee A$ \\
 $A\vee\neg A \equiv \top$ & $A\wedge\neg A \equiv \bot$ \\
 $A\rightarrow A \equiv \top$ \\
 $A\leftrightarrow A \equiv \top$ & $A\oplus A \equiv \bot$ \\
 $\neg A \equiv A\uparrow A$ & $\neg A \equiv A\downarrow A$ \\
 \\
 $A\vee B \equiv B\vee A$ & $A\wedge B \equiv B\wedge A$ \\
 $A\leftrightarrow B \equiv B\leftrightarrow A$ & $A\oplus B \equiv B\oplus A$ \\
 $A\uparrow B \equiv B\uparrow A$ & $A\downarrow B \equiv B\downarrow A$ \\
 $A\rightarrow B \equiv \neg B\rightarrow A$ \\
 \\
 $A\vee (B\vee C) \equiv (A\vee B)\vee C$ & $A\wedge (B\wedge C) \equiv (A\wedge B)\wedge C$ \\
 $A\leftrightarrow (B\leftrightarrow C) \equiv (A\leftrightarrow B)\leftrightarrow C$ & $A\oplus (B\oplus C) \equiv (A\oplus B)\oplus C$ \\
 \\
 $A\vee (B\wedge C) \equiv (A\vee B)\wedge (A\vee C)$ & $A\wedge (B\vee C) \equiv (A\wedge B)\vee (A\wedge C)$ \\
 $A\wedge (A\vee B) \equiv A$ & $A\vee (A\wedge B) \equiv A$ \\
 \\
 $A\leftrightarrow B \equiv (A\rightarrow B)\wedge (B\rightarrow A)$ & $A\oplus B \equiv \neg(A\rightarrow B)\vee \neg(B\rightarrow A)$ \\
 $A\rightarrow B \equiv \neg A\vee B$ & $A\rightarrow B \equiv \neg(A\wedge \neg B)$ \\
 $A\vee B \equiv \neg (\neg A\wedge \neg B)$ & $A\wedge B \equiv \neg(\neg A\vee \neg B)$ \\
 $A\vee B \equiv \neg A\rightarrow B$ & $A\wedge B \equiv \neg(A\rightarrow \neg B)$ \\
 \\
 $A\leftrightarrow B \equiv A\leftrightarrow (A\wedge B)$ & $A\rightarrow B \equiv B\leftrightarrow (A\vee B)$ \\
 $A\wedge B \equiv (A\leftrightarrow B)\leftrightarrow (A\vee B)$ & $A\leftrightarrow B \equiv (A\vee B)\rightarrow (A\wedge B)$ \\
\end{tabular}

\pagebreak

\noindent {\bf\Large Relacionamento entre os conceitos:
\begin{itemize}
 \item f\'ormula satisfat\'{\i}vel
 \item f\'ormula insatisfat\'{\i}vel (contradit\'oria)
 \item f\'ormula v\'alida (tautologia)
 \item f\'ormula n\~ao v\'alida (false\'avel)
\end{itemize}}

\vspace*{.5cm}
\begin{picture}(420,200) \bf
\put(-10,50){\framebox(420,80){contingentes}}
\put(130,130){\line(0,-1){80}}
\put(270,130){\line(0,-1){80}}

\put(60,90){\makebox(0,0){v\'alidas}}

\put(340,90){\makebox(0,0){contradit\'orias}}

\put(130,45){\line(0,-1){10}}
\put(135,35){\oval(10,10)[lb]}
\put(135,30){\line(1,0){270}}
\put(405,35){\oval(10,10)[rb]}
\put(410,45){\line(0,-1){10}}

\put(270,20){\makebox(0,0)[c]{false\'aveis}}

\put(-10,135){\line(0,1){10}}
\put(-5,145){\oval(10,10)[lt]}
\put(-5,150){\line(1,0){270}}
\put(265,145){\oval(10,10)[rt]}
\put(270,145){\line(0,-1){10}}

\put(130,160){\makebox(0,0)[c]{satisfat\'{\i}veis}}
\end{picture}
\pagebreak

\vspace*{1.5cm}
\noindent {\bf\Large M\'etodo da tabela da verdade/exemplo:}

\vspace*{.5cm}
\begin{tabular}{|c|c||c|c|c|c|} \hline
 $p$ & $q$ & $p\rightarrow q$  & $\neg(p\rightarrow q)$ & $\neg q$ & $\neg(p\rightarrow q)\rightarrow\neg q$ \\ \hline\hline
 V & V & V & F & F & V  \\ \hline
 V & F & F & V & V & V  \\ \hline
 F & V & V & F & F & V  \\ \hline
 F & F & V & F & V & V  \\ \hline
\end{tabular}
{\bf v\'alida}!

\vspace*{1.5cm}
\noindent {\bf\Large M\'etodo da tabela da verdade/exemplo:}

\vspace*{.5cm}
\begin{tabular}{|c|c||c|c|c|c|} \hline
 $p$ & $q$ & $p\rightarrow q$  & $\neg q$ & $p\wedge \neg q$ & $(p\rightarrow q)\wedge p\wedge \neg q$\\ \hline\hline
 V & V & V & F & F & F  \\ \hline
 V & F & F & V & V & F  \\ \hline
 F & V & V & F & F & F  \\ \hline
 F & F & V & V & F & F  \\ \hline
\end{tabular}
{\bf contradi\c c\~ao}!

 \vspace*{1.5cm}
\noindent {\bf\Large M\'etodo da tabela da verdade/exemplo:}

\vspace*{.5cm}
\begin{tabular}{|c|c||c|c|c|} \hline
 $p$ & $q$ & $p\rightarrow q$  & $\neg q$ & $(p\rightarrow q)\wedge\neg q$ \\ \hline\hline
 V & V & V & F & F  \\ \hline
 V & F & F & V & F  \\ \hline
 F & V & V & F & F  \\ \hline
 F & F & V & V & V  \\ \hline
\end{tabular}
{\bf conting\^encia}!

\pagebreak

\vspace*{1.5cm}
\noindent {\bf\Large Regras para tableaux sem\^anticos:}

\vspace*{1.5cm}
\noindent {\bf Regras }$\alpha$:

\vspace*{1cm}
\begin{tabular}{|c|c|c|} \hline
 $\alpha$ & $\alpha_1$ & $\alpha_2$ \\ \hline\hline
 $\neg\neg A_1$            & $A_1$      &             \\ \hline
 $A_1\wedge A_2$           & $A_1$      & $A_2$       \\ \hline
 $\neg(A_1\vee A_2)$       & $\neg A_1$ & $\neg A_2$  \\ \hline
 $\neg(A_1\rightarrow A_2)$& $A_1$      & $\neg A_2$  \\ \hline
 $\neg(A_1\uparrow A_2)$   & $A_1$      & $A_2$       \\ \hline
 $A_1\downarrow A_2$       & $\neg A_1$ & $\neg A_2$  \\ \hline
 $A_1\leftrightarrow A_2$  & $A_1\rightarrow A_2$ & $A_2\rightarrow A_1$  \\ \hline
 $\neg(A_1\oplus A_2)$     & $A_1\rightarrow A_2$ & $A_2\rightarrow A_1$  \\ \hline
\end{tabular}

\vspace*{1.5cm}
\noindent {\bf Regras }$\beta$:

\vspace*{1cm}
\begin{tabular}{|c|c|c|} \hline
 $\beta$ & $\beta_1$ & $\beta_2$ \\ \hline\hline
 \\ \hline
 $\neg(B_1\wedge B_2)$     & $\neg B_1$ & $\neg B_2$  \\ \hline
 $B_1\vee B_2$             & $B_1$      & $B_2$       \\ \hline
 $B_1\rightarrow B_2$      & $\neg B_1$ & $B_2$       \\ \hline
 $B_1\uparrow B_2$         & $\neg B_1$ & $\neg B_2$  \\ \hline
 $\neg(B_1\downarrow B_2)$ & $B_1$      & $B_2$       \\ \hline
 $\neg(B_1\leftrightarrow B_2)$ & $\neg(B_1\rightarrow B_2)$ & $\neg(B_2\rightarrow B_1)$  \\ \hline
 $B_1\oplus B_2$           & $\neg(B_1\rightarrow B_2)$ & $\neg(B_2\rightarrow B_1)$  \\ \hline
\end{tabular}

\pagebreak

\vspace*{1.5cm}
\noindent {\bf\Large Constru\c c\~ao de um tableau sem\^antico:}

\vspace*{1cm}
\begin{flushleft}
{\bf Entrada:} $A\in{\cal F}$. \\
{\bf Sa\'{\i}da:} tableau {\cal T} com toda folha marcada.
\end{flushleft}

\vspace*{.3cm}
\begin{tabbing}
xxx\=xxx\=xxx\=xxxx\= \kill
{\cal T} $:=$ um nodo n\~ao marcado rotulado com $\{A\}$. \\
{\bf repita} \\
 \> escolha uma folha {\em n\~ao marcada\/} $f$ de r\a'otulo $U(f)$; \\
 \> {\bf se} $U(f)$ \a'e um conjunto de literais {\bf ent\~ao} \\
 \> \> {\bf se} existe um par de literais complementares em $U(f)$ {\bf ent\~ao} \\
 \> \> \> marque $f$ como {\em fechado\/} $\times$ \\
 \> \> {\bf sen\~ao} \\
 \> \> \> marque $f$ como {\em aberto\/} $\odot$ \\
 \> \> {\bf fimse} \\
 \> {\bf sen\~ao} ($U(f)$ cont\a'em um n\~ao literal) \\
 \> \> escolha uma f\a'ormula $A$ em $U(f)$ que n\~ao seja literal; \\
 \> \> {\bf se} $A$ \a'e uma $\alpha$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> crie um nodo $f'$ como filho de $f$ com r\a'otulo: \\
 \> \> \> \> $U(f')=(U(f)-\{\alpha\})\cup\{\alpha_1,\alpha_2\}$ \\
 \> \> \> (no caso em que $A$ \a'e $\neg\neg A_1$, n\~ao h\a'a $\alpha_2$) \\
 \> \> {\bf sen\~ao} ($A$ \a'e uma $\beta$-f\a'ormula) \\
 \> \> \> crie dois nodos $f'$ e $f''$ como filhos de $f$ com r\a'otulos: \\
 \> \> \> \> $U(f')=(U(f)-\{\beta\})\cup\{\beta_1\}$ \\
 \> \> \> \> $U(f'')=(U(f)-\{\beta\})\cup\{\beta_2\}$ \\
 \> \> {\bf fimse} \\
 \> {\bf fimse} \\
{\bf at\a'e} toda folha est\a'a marcada.
\end{tabbing}


\end{document}
