\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

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


\noindent Defini\c c\~ao de {\em f\'ormula\/} e {\em f\'ormula at\^omica\/}:

\vspace*{.5cm}
\begin{tabular}{llll}
 {\em arg\/}        & $::=$ & $x$    & para qualquer $x\in {\cal V}$ \\
 {\em arg\/}        & $::=$ & $a$    & para qualquer $a\in {\cal A}$ \\
 {\em lista-args\/} & $::=$ & {\em arg\/} \\
 {\em lista-args\/} & $::=$ & {\em arg\/} , {\em lista-args\/} \\
 {\em fml-atom\/}   & $::=$ & $p$    &  para qualquer $p\in {\cal P}$ \\
 {\em fml-atom\/}   & $::=$ & $p(\mbox{\em lista-args})$
                                     & para qualquer $p\in {\cal P}$ \\
 {\em fml\/}        & $::=$ & {\em fml-atom\/} \\
 {\em fml\/}        & $::=$ & $\neg$ {\em fml\/} \\
 {\em fml\/}        & $::=$ & {\em fml\/} $\vee$ {\em fml\/} \\
                    & $\vdots$ \\
 {\em fml\/}        & $::=$ & {\em fml\/} $\leftrightarrow$ {\em fml\/} \\
 {\em fml\/}        & $::=$ & $\forall x$ {\em fml\/} & para qualquer $x\in {\cal V}$ \\
 {\em fml\/}        & $::=$ & $\exists x$ {\em fml\/} & para qualquer $x\in {\cal V}$ \\
\end{tabular}


\pagebreak
\noindent Exemplos de {\bf f\'ormulas}:

\vspace*{1.5cm}
\begin{enumerate}
 \item $\forall x\,\forall y\, (p(x,y)\rightarrow p(y,x))$

\vspace*{3mm}
 \item $\forall x\,\exists y\, p(x,y)$

\vspace*{3mm}
 \item $\exists x\,\exists y\, (p(x)\wedge \neg p(y))$

\vspace*{3mm}
 \item $\forall x\, p(a,x)$

\vspace*{3mm}
 \item $\forall x\,(p(x)\wedge q(x))\leftrightarrow (\forall x\, p(x)\wedge
                \forall x\, q(x))$

\vspace*{3mm}
 \item $\exists x\,(p(x)\vee q(x))\leftrightarrow (\exists x\, p(x)\vee
                \exists x\, q(x))$
 \item $\forall x\,(p(x)\rightarrow q(x))\rightarrow (\forall x\, p(x)\rightarrow
                \forall x\, q(x))$

\vspace*{3mm}
 \item $(\forall x\, p(x)\rightarrow \forall x\, q(x))\rightarrow (\forall x\, 
                (p(x)\rightarrow q(x))$
\end{enumerate}

\pagebreak
\noindent Exemplos de {\bf f\'ormulas v\'alidas}:

\vspace*{.5cm}
\begin{tabular}{ll}
$\forall x\,A(x)\leftrightarrow \neg \exists x\,\neg A(x)$ \\
$\exists x\,A(x)\leftrightarrow \neg \forall x\,\neg A(x)$ \\
 \\
$\forall x\,\forall y\,A(x,y)\leftrightarrow \forall y\,\forall x\,A(x,y)$ \\
$\exists x\,\exists y\,A(x,y)\leftrightarrow \exists y\,\exists x\,A(x,y)$ \\
$\exists x\,\forall y\,A(x,y)\rightarrow \forall y\,\exists x\,A(x,y)$ \\
 \\
$(Q x\,A(x)\vee B)\leftrightarrow Q x\,(A(x)\vee B)$ & $Q\in\{\forall,\exists\}$ \\
$(B\vee Q x\,A(x))\leftrightarrow Q x\,(B\vee A(x))$ & $Q\in\{\forall,\exists\}$ \\
 \\
$(Q x\,A(x)\wedge B)\leftrightarrow Q x\,(A(x)\wedge B)$ & $Q\in\{\forall,\exists\}$ \\
$(B\wedge Q x\,A(x))\leftrightarrow Q x\,(B\wedge A(x))$ & $Q\in\{\forall,\exists\}$ \\
 \\
$\forall x\,(A\rightarrow B(x))\leftrightarrow(A\rightarrow\forall x\,B(x))$ \\
$\forall x\,(A(x)\rightarrow B)\leftrightarrow(\exists x\,A(x)\rightarrow B)$ \\
 \\
$\exists x\,(A(x)\vee B(x))\leftrightarrow (\exists x\,A(x)\vee \exists x\,B(x))$ \\
$\forall x\,(A(x)\wedge B(x))\leftrightarrow (\forall x\,A(x)\wedge \forall x\,B(x))$ \\
 \\
$(\forall x\,A(x)\vee \forall x\,B(x))\rightarrow\forall x\,(A(x)\vee B(x))$ \\
 $\exists x\,(A(x)\wedge B(x))\rightarrow(\exists x\,A(x)\wedge\exists x\, B(x))$ \\
 \\
$\forall x\,(A(x)\leftrightarrow B(x))\rightarrow(\forall x\,A(x)\leftrightarrow \forall x\,B(x))$ \\
$\forall x\,(A(x)\leftrightarrow B(x))\rightarrow(\exists x\,A(x)\leftrightarrow \exists x\,B(x))$ \\
 \\
 $\exists x\,(A(x)\rightarrow B(x))\leftrightarrow(\forall x\,A(x)\rightarrow\exists x\, B(x))$ \\
 $(\exists x\,A(x)\rightarrow \forall x\,B(x))\rightarrow\forall x\,(A(x)\rightarrow B(x))$ \\
 \\
$\forall x\,(A(x)\vee B(x))\rightarrow(\forall x\,A(x)\vee \exists x\,B(x))$ \\
 \\
$\forall x\,(A(x)\rightarrow B(x))\rightarrow(\forall x\,A(x)\rightarrow \forall x\,B(x))$ \\
$\forall x\,(A(x)\rightarrow B(x))\rightarrow(\exists x\,A(x)\rightarrow \exists x\,B(x))$ \\
$\forall x\,(A(x)\rightarrow B(x))\rightarrow(\forall x\,A(x)\rightarrow \exists x\,B(x))$ \\
\end{tabular}

\addtolength{\topmargin}{-1cm}
\addtolength{\textheight}{3cm}

\pagebreak
\noindent {\bf\Large Constru\c c\~ao de um tableau sem\^antico:}

%\vspace*{2mm}
\begin{flushleft}
{\bf Entrada:} $A\in{\cal F}$. \\
{\bf Sa\'{\i}da:} tableau {\cal T} em que cada ramo \'e finito com toda folha marcada
como fechada ou aberta, ou \'e infinito.
\end{flushleft}

%\vspace*{2mm}
\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\~aose} $A$ \a'e uma $\beta$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> 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 sen\~aose} $A$ \a'e uma $\gamma$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> crie um nodo $f'$ como filho de $f$ com r\a'otulo: \\
 \> \> \> \> $U(f')=U(f)\cup\{\gamma(a)\}$ \\
 \> \> \> onde $a$ \a'e uma constante que {\em aparece\/} em $U(f)$; \\
 \> \> \> {\bf se} $U(f)$ s\a'o tem literais e f\a'ormulas $\gamma$ e $U(f')=U(f)$ {\bf ent\~ao} \\
 \> \> \> \>  marque $f$ como {\em aberto\/} $\odot$ \\
 \> \> \> {\bf fimse} \\
 \> \> {\bf sen\~aose} $A$ \a'e uma $\delta$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> crie um nodo $f'$ como filho de $f$ com r\a'otulo: \\
 \> \> \> \> $U(f')=(U(f)-\{A\})\cup\{\delta(a)\}$ \\
 \> \> \> onde $a$ \a'e uma constante que {\em n\~ao aparece\/} em $U(f)$ \\
 \> \> {\bf fimse} \\
 \> {\bf fimse} \\
{\bf at\a'e} toda folha est\a'a marcada.
\end{tabbing}

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

\addtolength{\topmargin}{-1.5cm}
\addtolength{\textheight}{4cm}
\addtolength{\oddsidemargin}{-1cm}
\addtolength{\evensidemargin}{-1cm}
\addtolength{\textwidth}{1cm}

\pagebreak
\noindent {\bf\Large Constru\c c\~ao sistem\'atica de um tableau sem\^antico:}

%\vspace*{2mm}
\begin{flushleft}
{\bf Entrada:} $A\in{\cal F}$. \\
{\bf Sa\'{\i}da:} tableau {\cal T} em que cada ramo \'e finito com toda folha marcada
como fechada ou aberta, ou \'e infinito.
\end{flushleft}

%\vspace*{2mm}
\begin{tabbing}
xxx\=xxx\=xxx\=xxx\=xxx\= \kill
{\cal T} $:=$ um nodo n\~ao marcado rotulado com $(\{A\},\{a_1,\ldots,a_k\})$ ou $(\{A\},\{a\})$. \\
{\bf repita} \\
 \> escolha uma folha {\em n\~ao marcada\/} $f$ de r\a'otulo $W(f)=(U(f),C(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 seja $\alpha$, $\beta$ ou $\delta$; \\
 \> \> {\bf se} encontrou tal $A$ {\bf ent\~ao} \\
 \> \> \> {\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: \\
 \> \> \> \> \> $W(f')=(U(f'),C(f'))=((U(f)-\{\alpha\})\cup\{\alpha_1,\alpha_2\},C(f))$ \\
 \> \> \> \> (no caso em que $A$ \a'e $\neg\neg A_1$, n\~ao h\a'a $\alpha_2$) \\
 \> \> \> {\bf sen\~aose} $A$ \a'e uma $\beta$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> \> crie dois nodos $f'$ e $f''$ como filhos de $f$ com r\a'otulos: \\
 \> \> \> \> \> $W(f')=(U(f'),C(f'))=((U(f)-\{\beta\})\cup\{\beta_1\},C(f))$ \\
 \> \> \> \> \> $W(f'')=(U(f''),C(f''))=((U(f)-\{\beta\})\cup\{\beta_2\},C(f))$ \\
 \> \> \> {\bf sen\~aose} $A$ \a'e uma $\delta$-f\a'ormula {\bf ent\~ao} \\
 \> \> \> \> crie um nodo $f'$ como filho de $f$ com r\a'otulo: \\
 \> \> \> \> \> $W(f')=(U(f'),C(f'))=((U(f)-\{A\})\cup\{\delta(a)\},C(f)\cup\{a\})$ \\
 \> \> \> \> onde $a$ \a'e uma constante que {\em n\~ao aparece\/} em $U(f)$ \\
 \> \> \> {\bf fimse} \\
 \> \> {\bf sen\~ao} \\
 \> \> \> sejam $\{\gamma_1,\ldots\gamma_m\}\subseteq U(f)$ todas as f\a'ormulas $\gamma$ em $U(f)$; \\
 \> \> \> seja $C(f)=\{a_1,\ldots,a_k\}$; \\
 \> \> \> crie um nodo $f'$ como filho de $f$ com r\a'otulo: \\
 \> \> \> \> $W(f')=(U(f'),C(f'))=(U(f)\cup_{i=1\,\,\,j=1}^{i=m\,j=k}\{\gamma_i(a_j)\},C(f))$; \\
 \> \> \> {\bf se} $U(f)$ s\a'o tem literais e f\a'ormulas $\gamma$ e $U(f')=U(f)$ {\bf ent\~ao} \\
 \> \> \> \>  marque $f$ como {\em aberto\/} $\odot$ \\
 \> \> \> {\bf fimse} \\
 \> \> {\bf fimse} \\
 \> {\bf fimse} \\
{\bf at\a'e} toda folha est\a'a marcada.
\end{tabbing}


\end{document}
