\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

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

\noindent {\bf\Large O Sistema de Gentzen {\cal G}:}

\vspace*{.5cm}
\begin{itemize}
 \item {\bf Axiomas:} conjuntos de f\'ormulas com um par de literais complementares.

\vspace*{5mm}
 \item {\bf Regras de infer\^encia:}

\vspace*{3mm}
      \begin{tabular}{cccc}
       $\vdash U_1\cup\{\alpha_1,\alpha_2\}$ & \hspace*{2cm} & $\vdash U_1\cup\{\beta_1\}$
                                       & $\vdash U_2\cup\{\beta_2\}$ \\ \cline{1-1}\cline{3-4}
       $\vdash U_1\cup\{\alpha\}$ &  & \multicolumn{2}{c}{$\vdash U_1\cup U_2\cup\{\beta\}$}
      \end{tabular}
\end{itemize}

\vspace*{.5cm}
\noindent {\bf F\'ormulas }$\alpha$:

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

\vspace*{.5cm}
\noindent {\bf F\'ormulas }$\beta$:

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

\pagebreak

\noindent {\bf\Large Ex. de dedu\c c\~ao no sistema {\cal G}:}

\vspace*{1cm}
\begin{tabular}{rlr}
 1. & $\vdash \neg p, p, q$      & Axioma \\
 2. & $\vdash \neg p, (p\vee q)$ & $\alpha\vee, 1$ \\
 3. & $\vdash \neg p, p, r$      & Axioma \\
 4. & $\vdash \neg p, (p\vee r)$ & $\alpha\vee, 3$ \\
 5. & $\vdash \neg p, (p\vee q)\wedge(p\vee r)$ & $\beta\wedge, 2, 4$ \\
 6. & $\vdash \neg q, \neg r, p, q$ & Axioma \\
 7. & $\vdash \neg q, \neg r, (p\vee q)$ & $\alpha\vee, 6$ \\
 8. & $\vdash \neg q, \neg r, p, r$ & Axioma \\
 9. & $\vdash \neg q, \neg r, (p\vee r)$ & $\alpha\vee, 8$ \\
10. & $\vdash \neg q, \neg r, (p\vee q)\wedge(p\vee r)$ & $\beta\wedge, 7, 9$ \\
11. & $\vdash \neg (q\wedge r), (p\vee q)\wedge(p\vee r)$ & $\alpha\wedge, 10$ \\
12. & $\vdash \neg (p\vee (q\wedge r)), (p\vee q)\wedge(p\vee r)$ & $\beta\vee, 5, 11$ \\
13. & $\vdash (p\vee (q\wedge r))\rightarrow(p\vee q)\wedge(p\vee r)$ & $\alpha\rightarrow, 12$
\end{tabular}

\pagebreak

\noindent {\bf\Large O sistema de Hilbert {\cal H}:}

\vspace*{.5cm}
\begin{itemize}
 \item {\bf Axioma 1:}

\vspace*{5mm}
       \hspace*{1cm}$\vdash A\rightarrow (B\rightarrow A)$.

\vspace*{5mm}
 \item {\bf Axioma 2:}

\vspace*{5mm}
       \hspace*{1cm}$\vdash (A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)
               \rightarrow(A\rightarrow C))$.

\vspace*{5mm}
 \item {\bf Axioma 3:}

\vspace*{5mm}
       \hspace*{1cm}$\vdash (\neg B\rightarrow\neg A)\rightarrow(A\rightarrow B)$.

\vspace*{5mm}
 \item {\bf Regra de infer\^encia:}

\vspace*{3mm}
      \begin{center}
      \begin{tabular}{ccc}
       $\vdash A$ & \hspace*{1cm} & $\vdash A\rightarrow B$ \\ \hline
        \multicolumn{3}{c}{$\vdash B$}
      \end{tabular}
      \end{center}

\end{itemize}

\vspace*{1.5cm}
\noindent{\bf\Large Exemplo: dedu\c c\~ao de } $A\rightarrow A$: 

\vspace*{1cm}
\noindent \begin{tabular}{rlr}
 1. & $\vdash (A\rightarrow ((A\rightarrow A)\rightarrow A))\rightarrow((A\rightarrow (A\rightarrow A))
               \rightarrow(A\rightarrow A))$      & Axioma 2\\
 2. & $\vdash A\rightarrow ((A\rightarrow A)\rightarrow A)$ & Axioma 1 \\
 3. & $\vdash (A\rightarrow (A\rightarrow A))\rightarrow(A\rightarrow A)$ & MP 1,2 \\
 4. & $\vdash A\rightarrow (A\rightarrow A)$ & Axioma 1 \\
 5. & $\vdash A\rightarrow A$ & MP 3,4 \\
\end{tabular}

\pagebreak
\noindent {\bf\Large Procedimento de resolu\c c\~ao:}

\vspace*{.5cm}
\begin{flushleft}
{\bf Entrada:} um conjunto de cl\'ausulas $S$. \\
{\bf Sa\'{\i}da:} $S$ \'e satisfat\'{\i}vel ou n\~ao.
\end{flushleft}

\vspace*{.3cm}
\begin{tabbing}
xxx\=xxx\=xxx\=xxxx\= \kill
$R$ $:=$ $S$; \\
{\bf la\c co} \\
 \> escolha $C_1$ e $C_2$ em $R$ com literais complementares {\em n\~ao escolhidos ainda\/}; \\
 \> {\bf se} tais $C_1$ e $C_2$ n\~ao existirem {\bf ent\~ao} \\
 \> \> retorne {\em $S$ \a'e satisfat\a'{\i}vel} \\
 \> {\bf fimse}; \\
 \> $C$ $:=$ $\mbox{res}(C_1,C_2)$; \\
 \> $R$ $:=$ $R\cup\{C\}$; \\
 \> {\bf se} $C=\Box$ {\bf ent\~ao} \\
 \> \> retorne {\em $S$ \a'e insatisfat\a'{\i}vel} \\
 \> {\bf fimse}; \\
{\bf fimla\c co}.
\end{tabbing}

\vspace*{1.5cm}
\noindent {\bf\Large Um exemplo de R.M. Smullyan:}\footnote{What is the Name of
              this Book? The riddle of Dracula and other logical puzzles,
              Simon \& Schuster, 1978}

\begin{enumerate}
 \item Se $A$ \'e culpado e $B$ \'e inocente, ent\~ao $C$ \'e culpado.
 \item $C$ nunca trabalha sozinho.
 \item $A$ nunca trabalha com $C$.
 \item Pelo menos um dos tr\^es \'e culpado, j\'a que ningu\'em mais
       esteve envolvido.
\end{enumerate}

Quem \'e necessariamente culpado?

\end{document}
