\documentclass[12pt, a4paper]{article}
 
\newcounter{conta}
\newcounter{conta2}

\hyphenation{e-xem-plo pro-je-to di-fe-ren-te
com-ple-xi-da-de de-sa-pa-re-ce a-bor-da-gem co-mo}

\begin{document}

\vspace*{9cm}
\begin{center} \Huge\bf
Cap\'{\i}tulo 9: Infer\^encia em L\'ogica de Primeira Ordem
\end{center}

\vfill
\pagebreak
\noindent{\Huge\bf Regras de Infer\^encia}

\vspace*{1cm}
\noindent {\LARGE Exemplos para parte proposicional:}

\begin{enumerate}\Large
 \item[\ ] {\em Modus Ponens\/} (MP):

              \[\frac{\alpha\,\, \alpha\Rightarrow\beta}{\beta}\]

               \[\frac{\mbox{em}(\mbox{Jo\~ao},\mbox{DCC})\,\,\,\,\mbox{em}(\mbox{Jo\~ao},
                 \mbox{DCC})\Rightarrow\mbox{OK}(\mbox{Jo\~ao})}{\mbox{OK}(\mbox{Jo\~ao})}\]
 \item[\ ] Introdu\c c\~ao do ``e'' (IE):

              \[\frac{\alpha\,\,\,\,\,\,\beta}{\alpha\wedge\beta}\]

               \[\frac{\mbox{OK}(\mbox{Jo\~ao})\,\,\,\,\mbox{estuda}(\mbox{Jo\~ao},\mbox{CC})}
                 {\mbox{OK}(\mbox{Jo\~ao})\wedge\mbox{estuda}(\mbox{Jo\~ao},\mbox{CC})}\]

 \item[\ ] Elimina\c c\~ao do ``e'' (EE):

              \[\frac{\alpha\wedge\beta}{\alpha}\hspace*{1cm}\frac{\alpha\wedge\beta}{\beta}\]

\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE Etc...}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE Envolvendo quantificadores:}

\begin{enumerate}\Large
 \item[\ ] Elimina\c c\~ao do universal (EUn):

              \[\frac{\forall x\, \alpha}{\alpha \{x/t\}}\] onde $t$ \'e um termo sem vari\'aveis.

               \[\frac{\forall x\,\, \mbox{em}(x,\mbox{DCC})\Rightarrow\mbox{OK}(x)}
                        {\mbox{em}(\mbox{Jo\~ao},\mbox{DCC})\Rightarrow\mbox{OK}(\mbox{Jo\~ao})}\]
 \item[\ ] Elimina\c c\~ao do existencial (EEx):

              \[\frac{\exists x\, \alpha}{\alpha \{x/k\}}\] onde $t$ \'e uma constante {\bf nova}.

               \[\frac{\exists x\,\,\mbox{estuda}(x,\mbox{CC})\wedge  \mbox{feliz}(x)}
                        {\mbox{estuda}(\mbox{A},\mbox{CC})\wedge\mbox{feliz}(\mbox{A})}\]

 \item[\ ] Introdu\c c\~ao do existencial (IEx):

              \[\frac{\alpha}{\exists x\,\alpha\{t/x\}}\] onde $t$ \'e um termo sem vari\'aveis.

               \[\frac{\mbox{feliz}(\mbox{Jo\~ao})}
                        {\exists x\,\,\mbox{feliz}(x)}\]

\end{enumerate}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Um exemplo de Prova}

\vspace*{1cm}
\begin{enumerate} \Large\em
 \item[1.] Bob \'e um boi.
 \item[2.] Pat \'e um porco.
 \item[3.] Bois s\~ao mais velozes que porcos.
 \item[\ ] De 1, 2 e 3: Bob \'e mais veloz que Pat.
\end{enumerate}

\vspace*{1cm}
\begin{enumerate} \Large
 \item[1.] $\mbox{boi}(\mbox{Bob})$
 \item[2.] $\mbox{porco}(\mbox{Pat})$
 \item[3.] $\forall x,y [\mbox{boi}(x)\wedge\mbox{porco}(y)\Rightarrow\mbox{m-veloz}(x,y)]$
 \item[4.] $\mbox{boi}(\mbox{Bob})\wedge\mbox{porco}(\mbox{Pat})$ por IE (1, 2)
 \item[5.] $\mbox{boi}(\mbox{Bob})\wedge\mbox{porco}(\mbox{Pat})\Rightarrow\mbox{m-veloz}
            (\mbox{Bob},\mbox{Pat})$ por EUn (3)
 \item[6.] $\mbox{m-veloz}(\mbox{Bob},\mbox{Pat})$ por MP (4, 5)
\end{enumerate}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE Busca com regras de infer\^encia primitivas:}

\vspace*{.5cm}
\begin{itemize} \Large
 \item {\bf Estados:} conjuntos de senten\c cas.
 \item {\bf Operadores:} regras de infer\^encia.
 \item {\bf Teste de meta:} estado cont\'em senten\c ca relativa \`a consulta.
\end{itemize}

\vspace*{.5cm}
\noindent {\LARGE $\Rightarrow$ {\bf Problema:} fator de ramifica\c c\~ao enorme.}

\vspace*{1cm}
\noindent {\LARGE Padr\~ao inferencial do exemplo anterior:}

\begin{itemize}
 \item {\LARGE IE, EUn, MP}
\end{itemize}
{\LARGE $\Rightarrow$ bastante comum!}

\vspace*{1cm}
\noindent {\Large De}
\begin{enumerate} \Large
 \item[\ ] $\mbox{boi}(\mbox{Bob})$,
 \item[\ ] $\mbox{porco}(\mbox{Pat})$, e
 \item[\ ] $\forall x,y [\mbox{boi}(x)\wedge\mbox{porco}(y)\Rightarrow\mbox{m-veloz}(x,y)]$
\end{enumerate}
{\Large deduzir:}
\begin{enumerate} \Large
 \item[\ ] $\mbox{m-veloz}(\mbox{Bob},\mbox{Pat})$
\end{enumerate}
{\Large por MP {\bf generalizada}.}

\vfill
\hfill Cap\'{\i}tulo 9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Unifica\c c\~ao:}

\vspace*{1cm}
\noindent {\LARGE $\sigma$ {\bf unifica} senten\c cas at\^omicas $p$ e $q$
  se $p\sigma=q\sigma$.}

\vspace*{.5cm}
\noindent {\LARGE Exemplos:}

\begin{itemize}\Large
 \item $p=\mbox{conhece}(\mbox{Jo\~ao},x)$ e $q_1=\mbox{conhece}(\mbox{Jo\~ao},\mbox{Joana})$
 \item $p=\mbox{conhece}(\mbox{Jo\~ao},x)$ e $q_2=\mbox{conhece}(y,\mbox{Jorge})$
 \item $p=\mbox{conhece}(\mbox{Jo\~ao},x)$ e $q_3=\mbox{conhece}(y,\mbox{m\~ae}(y))$
 \item $p=\mbox{conhece}(\mbox{Jo\~ao},x)$ e $q_4=\mbox{conhece}(x,\mbox{Joana})$
\end{itemize}

\vspace*{1cm}
\noindent {\LARGE Id\'eia:}

\begin{enumerate}\Large
 \item Unificar premissas de uma regra com fatos.
 \item Aplicar unificador \`a conclus\~ao da regra.
\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE Exemplo: sabendo-se $q_1$, $q_2$ e $q_3$ e}

\begin{center}\Large
 $\mbox{conhece}(\mbox{Jo\~ao},x)\Rightarrow\mbox{gosta}(\mbox{Jo\~ao},x)$
\end{center}

\noindent {\LARGE conclui-se:}

\begin{itemize}\Large
 \item $\mbox{gosta}(\mbox{Jo\~ao},\mbox{Joana})$
 \item $\mbox{gosta}(\mbox{Jo\~ao},\mbox{Jorge})$
 \item $\mbox{gosta}(\mbox{Jo\~ao},\mbox{m\~ae}(\mbox{Jo\~ao}))$
\end{itemize}

\vfill
\hfill Cap\'{\i}tulo 9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Modus Ponens Generalizado (MPG):}

\vspace*{1cm}
{\Large
\[\frac{p_1'\,\, p_2'\,\, \ldots\,\, p_n'\,\, 
(p_1\wedge p_2\wedge\ldots\wedge p_n\Rightarrow q)}{q\sigma}
 \,\,\mbox{ onde $p_i'\sigma=p_i\sigma$.}\]
}

\vspace*{1cm}
\noindent{\LARGE Exemplo:}

\vspace*{1cm}
\noindent {\Large De:}

\begin{enumerate}\Large
 \item[\ ] $p_1'=\mbox{m-veloz}(\mbox{Bob},\mbox{Pat})$
 \item[\ ] $p_2'=\mbox{m-veloz}(\mbox{Pat},\mbox{Bill})$
 \item[\ ] $p_1\wedge p_2\Rightarrow q$ \\
              \hspace*{1cm}$=\mbox{m-veloz}(x,y)\wedge\mbox{m-veloz}(y,z)\Rightarrow \mbox{m-veloz}(x,z)$
\end{enumerate}

\noindent {\Large conclui-se ($\sigma=\{x/\mbox{Bob},y/\mbox{Bill}\}$):}

\begin{enumerate}\Large
\item[\ ] $q\sigma=\mbox{m-veloz}(\mbox{Bob},\mbox{Bill})$
\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE MPG \'e usada com BC que tem as caracter\'{\i}sticas: }

\begin{itemize}\Large
 \item Cada senten\c ca \'e uma {\bf cl\'ausula definida}.
 \item Todas as vari\'aveis s\~ao {\bf universalmente quantificadas}.
\end{itemize}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE Dois tipos de {\bf algoritmos de infer\^encia}:}

\begin{itemize}\Large
 \item {\em Forward chaining}
 \item {\em Backward chaining}
\end{itemize}

\vspace*{1.5cm}
\noindent {\LARGE\bf Forward chaining }

\vspace*{1cm}
\noindent {\Large Disparado quando um novo fato $p$ \'e adicionado \`a BC:}

\begin{enumerate}\Large
 \item[\ ] Para cada regra tal que $p$ unifica com uma de suas premissas, \\
         \hspace*{.5cm}se as outras premissas s\~ao \underline{conhecidas} \\
         \hspace*{.5cm}ent\~ao acrescente a conclus\~ao \`a BC \\
         \hspace*{1cm}e continue \ldots
\end{enumerate}
\begin{itemize}\Large
 \item {\em Forward chaining\/} \'e dirigido por \underline{dados}: infere propriedades
       e categorias a partir dos est\'{\i}mulos.
 \item Cada vez que a BC recebe uma senten\c ca (via TELL), \'e disparado.
\end{itemize}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Exemplo de Forward chaining:}

\vspace*{.5cm}
\begin{enumerate} \Large
\item[a)] BC $\Leftarrow$ [1] \underline{$\mbox{boi}(x)\wedge \mbox{porco}(y)\Rightarrow \mbox{m-veloz}(x,y)$}.

\item[b)] BC $\Leftarrow$ [2] \underline{$\mbox{porco}(y)\wedge \mbox{lesma}(z)\Rightarrow \mbox{m-veloz}(y,z)$}.

\item[c)] BC $\Leftarrow$ [3] \underline{$\mbox{m-veloz}(x,y)\wedge \mbox{m-veloz}(y,z)\Rightarrow \mbox{m-veloz}(x,z)$}.

\item[d)] BC $\Leftarrow$ [4] \underline{$\mbox{boi}(\mbox{Bob})$};

          un 4 com [1,a]: $\mbox{porco}(y)\Rightarrow \mbox{m-veloz}(\mbox{Bob},y)$.

\item[e)] BC $\Leftarrow$ [5] \underline{$\mbox{porco}(\mbox{Pat})$};

          un 5 com [1,b]: $\mbox{boi}(x)\Rightarrow \mbox{m-veloz}(x,\mbox{Pat})$,

          un com [4]: $\mbox{m-veloz}(\mbox{Bob},\mbox{Pat})$;

          \hspace*{5mm}BC $\Leftarrow$ [6] \underline{$\mbox{m-veloz}(\mbox{Bob},\mbox{Pat})$};

          \hspace*{5mm}un 6 com [3,a], \ldots. un 6 com [3,b], \ldots.

          un 5 com [2,a]: $\mbox{lesma}(z)\Rightarrow \mbox{m-veloz}(\mbox{Pat},z)$.


\item[f)] BC $\Leftarrow$ [7] \underline{$\mbox{lesma}(\mbox{Bill})$};

          un 7 com [2,b], un com [5]: $\mbox{m-veloz}(\mbox{Pat},\mbox{Bill})$;

          \hspace*{5mm}BC $\Leftarrow$ [8] \underline{$\mbox{m-veloz}(\mbox{Pat},\mbox{Bill})$};

          \hspace*{5mm}un 8 com [3,a]: $\mbox{m-veloz}(\mbox{Bill},z)\Rightarrow \mbox{m-veloz}(\mbox{Pat},z)$.

          \hspace*{5mm}un 8 com [3,b]: $\mbox{m-veloz}(x,\mbox{Pat})\Rightarrow \mbox{m-veloz}(x,\mbox{Bill})$,

          \hspace*{5mm}un com [6]: BC $\Leftarrow$ [9] \underline{$\mbox{m-veloz}(\mbox{Bob},\mbox{Bill})$};

          \hspace*{10mm}un [9] com [3,a], \ldots. un [9] com [3,b], \ldots.

\end{enumerate}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Backward chaining }

\vspace*{1cm}
\noindent {\Large Disparado para encontrar resposta(s) a uma consulta \`a BC:}

\begin{enumerate}\Large
 \item[\ ] Para uma consulta $q$: \\
         \hspace*{.5cm}se $q$ unifica com um fato $q'$, retorne o unificador; \\
         \hspace*{.5cm}para cada regra cujo consequente $q'$ unifica com $q$, \\
         \hspace*{1cm}tente provar cada premissa da regra por backward chaining.
\end{enumerate}

\begin{itemize}\Large
 \item Complica\c c\~oes maiores;
       \begin{itemize}
        \item Lidar com unifica\c c\~ao.
        \item Evitar {\em loops\/}.
       \end{itemize}
 \item Cada vez que a BC recebe uma consulta (via ASK), \'e disparado.
 \item Duas vers\~oes:
       \begin{itemize}
        \item Encontrar \underline{qualquer} solu\c c\~ao.
        \item Encontrar \underline{todas} as solu\c c\~oes.
       \end{itemize}
 \item \'E o algoritmo base de Prolog.
\end{itemize}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Exemplo de Backward chaining:}

\vspace*{.5cm}
\begin{enumerate}\Large
 \item[1.] $\mbox{porco}(y)\wedge \mbox{lesma}(z)\Rightarrow \mbox{m-veloz}(y,z)$
 \item[2.] $\mbox{viscoso}(z)\wedge \mbox{rasteja}(z)\Rightarrow \mbox{lesma}(z)$
 \item[3.] $\mbox{porco}(\mbox{Pat})$
 \item[4.] $\mbox{viscoso}(\mbox{Bill})$
 \item[5.] $\mbox{rasteja}(\mbox{Pat})$
 \item[6.] $\mbox{rasteja}(\mbox{Bill})$
\end{enumerate}

\vspace*{.5cm}
\noindent {\LARGE \'Arvore de Prova:}

\begin{picture}(400,220) \large
 \put(80,160){\framebox(120,20)[c]{$\mbox{m-veloz}(\mbox{Pat},\mbox{Bill})$}}
 \put(140,160){\line(-2,-1){80}}
 \put(140,160){\line(2,-1){80}}
 \put(210,160){\makebox(0,0)[l]{\boldmath $\{y/\mbox{Pat},z/\mbox{Bill}\}$}}

 \put(20,100){\framebox(80,20)[c]{$\mbox{porco}(\mbox{Pat})$}}
 \put(10,100){\makebox(0,0)[r]{\boldmath $\{\}$}}

 \put(180,100){\framebox(80,20)[c]{$\mbox{lesma}(\mbox{Bill})$}}
 \put(220,100){\line(-2,-1){80}}
 \put(220,100){\line(2,-1){80}}
 \put(310,100){\makebox(0,0)[l]{\boldmath $\{z/\mbox{Bill}\}$}}

 \put(100,40){\framebox(80,20)[c]{$\mbox{viscoso}(\mbox{Bill})$}}
 \put(90,40){\makebox(0,0)[r]{\boldmath $\{\}$}}

 \put(260,40){\framebox(80,20)[c]{$\mbox{rasteja}(\mbox{Bill})$}}
 \put(350,40){\makebox(0,0)[l]{\boldmath $\{\}$}}

\end{picture}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Corre\c c\~ao e completude:}

\vspace*{1cm}
\begin{itemize}\Large
 \item {\em Forward\/} e {\em backward chaining\/} s\~ao corretos e {\bf completos} para BC's
       do tipo Horn (cl\'ausulas definidas).
 \item {\em Forward\/} e {\em backward chaining\/} s\~ao corretos, mas {\bf incompletos} para
       l\'ogica de primeira ordem em geral.

       \vspace*{.5cm}
       BC:
       \begin{enumerate}
        \item $\mbox{doutor}(x)\Rightarrow\mbox{altamente-qualificado}(x)$
        \item $\neg\mbox{doutor}(x)\Rightarrow\mbox{trabalha-cedo}(x)$
        \item $\mbox{altamente-qualificado}(x)\Rightarrow\mbox{rico}(x)$
        \item $\mbox{trabalha-cedo}(x)\Rightarrow\mbox{rico}(x)$
       \end{enumerate}

       \vspace*{.5cm}
       BC $\models \mbox{rico}(\mbox{Eu})$, mas BC $\not\vdash_i \mbox{rico}(\mbox{Eu})$ se $i$ \'e qualquer um dos
       dois algoritmos.

       \vspace*{.5cm}
       Outra BC:
       \begin{enumerate}
        \item $\mbox{crian\c ca}(x)\Rightarrow\mbox{tomar}(x,\mbox{Krlgsuem})$
        \item $\neg\mbox{crian\c ca}(x)\Rightarrow\mbox{tomar}(x,\mbox{Ysoftars})$
       \end{enumerate}

       \vspace*{.5cm}
       BC $\models \mbox{tomar}(\mbox{Eu},\mbox{Krlgsuem})\vee\mbox{tomar}(\mbox{Eu},\mbox{Ysoftars})$.

\end{itemize}


\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\Huge\bf Resolu\c c\~ao}

\vspace*{1cm}
\begin{itemize}\Large
 \item Consequ\^encia l\'ogica \'e indecid\'{\i}vel; \'e semi-decid\'{\i}vel:

       \begin{itemize}
        \item \'E poss\'{\i}vel encontrar prova de $\alpha$ se $\mbox{BC}\models\alpha$.
        \item N\~ao \'e sempre poss\'{\i}vel determinar que  $\mbox{BC}\not\models\alpha$.
       \end{itemize}

       (Como no problema da parada.)

 \item Resolu\c c\~ao \'e um procedimento de {\bf refuta\c c\~ao}:

       \begin{itemize}
        \item Para provar $\mbox{BC}\models\alpha$, mostrar que $\mbox{BC}\wedge\neg\alpha$ \'e
              insatisfat\'{\i}vel.
       \end{itemize}

 \item Resolu\c c\~ao usa $\mbox{BC}\wedge\neg\alpha$ na FNC (conjun\c c\~ao de cl\'ausulas).

 \item A regra de resolu\c c\~ao obt\'em uma cl\'ausula a partir de duas outras: \[\frac{C_1\,\,\,C_2}{C}\]

 \item Meta: encontrar {\bf cl\'ausula vazia} (contradi\c c\~ao).

\end{itemize}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf A regra de infer\^encia Resolu\c c\~ao}

\vspace*{1cm}
\noindent {\LARGE Vers\~ao proposicional b\'asica:}

\vspace*{.5cm}
\begin{center}\Large
 $\frac{\alpha\vee\beta \,\,\, \neg\beta\vee\gamma}{\alpha\vee\gamma}$ \ \ \ ou ent\~ao \ \ \ 
 $\frac{\neg\alpha\Rightarrow\beta \,\,\, \beta\Rightarrow\gamma}{\neg\alpha\Rightarrow\gamma}$
\end{center}

\vspace*{1cm}
\noindent {\LARGE Vers\~ao de primeira ordem completa (cl\'ausulas):}

\vspace*{.5cm}
\begin{center}\Large
 $\frac{p_1\vee\ldots p_j\ldots\vee p_m \hspace*{1cm} q_1\vee\ldots q_k\ldots\vee q_n}
  {(p_1\vee\ldots p_{j-1}\vee p_{j+1}\ldots\vee p_m \vee q_1\vee\ldots q_{k-1}\vee q_{k+1}\ldots\vee q_n)\sigma}$
\end{center}
{\Large onde $p_j\sigma=\neg q_k\sigma$.}

\vspace*{1cm}
\noindent {\LARGE Exemplo:}

\vspace*{.5cm}
\begin{center}\Large
 $\frac{\neg \mbox{rico}(x)\vee\mbox{infeliz}(x)\hspace*{1cm} \mbox{rico}(\mbox{Eu})}{\mbox{infeliz}(\mbox{Eu})}$
\end{center}
{\Large com umg $\{x/\mbox{Eu}\}$.}

\vspace*{1cm}
\noindent {\LARGE Vers\~ao de primeira ordem completa (implica\c c\~oes):}

\vspace*{.5cm}
\begin{center}\Large
 $\frac{p_1\wedge\ldots p_j\ldots\wedge p_{n_1}\Rightarrow r_1\vee\ldots r_{n_2}\hspace*{1cm} 
   s_1\wedge\ldots s_{n_3}\Rightarrow q_1\vee\ldots q_k\ldots\vee q_{n_4}}
   {(p_1\wedge\ldots p_{j-1}\wedge p_{j+1}\ldots\wedge p_{n_1}\wedge s_1\wedge\ldots s_{n_3}\Rightarrow
    r_1\vee\ldots r_{n_2}\vee q_1\vee\ldots q_{k-1}\vee q_{k+1}\ldots\vee q_{n_4})\sigma}$
\end{center}
{\Large onde $p_j\sigma=q_k\sigma$.}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE Formas normais para Resolu\c c\~ao: }

\vspace*{.5cm}
\begin{itemize}\Large
 \item Forma normal conjuntiva (FNC): conjun\c c\~ao de \underline{cl\'ausulas} da forma:

         \begin{enumerate}
          \item[\ ] $p_1\vee p_2\vee\ldots\vee p_n$
          \item[\ ] onde cada $p_i$ \'e um \underline{literal}.
         \end{enumerate}

 \item Forma normal implicativa (FNI): conjun\c c\~ao de \underline{implica\c c\~oes} da forma:

         \begin{enumerate}
          \item[\ ] $p_1\wedge p_2\wedge\ldots\wedge p_m\Rightarrow q_1\vee q_2\vee\ldots\vee q_n$
          \item[\ ] onde cada $p_i$ e cada $q_j$ \'e uma \underline{senten\c ca at\^omica}.
         \end{enumerate}
\end{itemize}

\vspace*{1cm}
\noindent {\LARGE Exemplos: }

\vspace*{.5cm}
{\Large
\begin{tabular}{ll}
 {\em Cl\'ausulas} & {\em Implica\c c\~oes} \\
 $\neg p(x)\vee q(x)$ & $p(x)\Rightarrow q(x)$ \\
 $\neg p(x)\vee q(x)\vee\neg r(x)\vee s(x)$ & $p(x)\wedge r(x)\Rightarrow q(x)\vee s(x)$ \\
 $p(x)\vee q(x)$ & $\mbox{\bf V}\Rightarrow p(x)\vee q(x)$ \\
 $\neg p(x)\vee\neg q(x)$ & $p(x)\wedge q(x)\Rightarrow \mbox{\bf F}$
\end{tabular}
}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Convers\~ao de uma senten\c ca para FNC:}

\vspace*{.5cm}
\begin{enumerate}\Large
 \item Eliminar ``$\Rightarrow$'':
         \begin{enumerate}
          \item[\ ] $\alpha\Rightarrow\beta$ por $\neg\alpha\vee\beta$
         \end{enumerate}
 \item Mover ``$\neg$'' para dentro:
         \begin{enumerate}
          \item[\ ] $\neg\neg\alpha$ por $\alpha$
          \item[\ ] $\neg(\alpha\wedge\beta)$ por $\neg\alpha\vee\neg\beta$
          \item[\ ] $\neg(\alpha\vee\beta)$ por $\neg\alpha\wedge\neg\beta$
          \item[\ ] $\neg\forall x\alpha$ por $\exists x\neg\alpha$
          \item[\ ] $\neg\exists x\alpha$ por $\forall x\neg\alpha$
         \end{enumerate}
 \item Colocar cada quantificador com uma vari\'avel diferente.
 \item Eliminar os quantificadores existenciais (Skolemiza\c c\~ao):
         \begin{enumerate}
          \item[\ ] Tirar $\exists x$ e substituir $x$ por $f(y_1,y_2,\ldots,y_n)$ se $x$
                       est\'a no escopo de quantificadores universais $\forall y_1\forall y_2\ldots\forall y_n$
                       (ver pr\'oxima transpar\^encia).
         \end{enumerate}
 \item Eliminar os quantificadores universais.
 \item Distribuir $\wedge$ sobre $\vee$:
         \begin{enumerate}
          \item[\ ] $(\alpha\wedge\beta)\vee\gamma$ por $(\alpha\vee\gamma)\wedge(\beta\vee\gamma)$
         \end{enumerate}
\end{enumerate}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Skolemiza\c c\~ao/Exemplos:}

\vspace*{1cm}
\begin{itemize}\Large
 \item $\exists x \,\,\mbox{feliz}(x)$ torna-se $\mbox{feliz}(\mbox{C})$

          C: {\em constante de Skolem}.
 \item $\forall x\exists y \,\,\mbox{ama}(x,y)$ torna-se $\forall x\,\,\mbox{ama}(x,f(x))$

          $f$: {\em fun\c c\~ao de Skolem}.
 \item $\forall x\,\,\mbox{pessoa}(x)\Rightarrow\exists y\,\, \mbox{cora\c c\~ao}(y)\wedge\mbox{tem}(x,y)$ torna-se
          $\forall x\,\,\mbox{pessoa}(x)\Rightarrow\mbox{cora\c c\~ao}(c(x))\wedge\mbox{tem}(x,c(x))$

          $c$: {\em fun\c c\~ao de Skolem}.
 \item $\forall x\exists y\forall z\exists w p(x,y,z,w)$ por $\forall x\forall z p(x,f(x),z,g(x,z))$

          $f$ e $g$: {\em fun\c c\~oes de Skolem}.
 \item $\exists x\forall y[\forall z (p(x,y)\vee q(y,z))\Rightarrow \exists w r(x,y,w)]$ por:

         $\exists x\forall y[\neg(\forall z (p(x,y)\vee  q(y,z))\vee \exists w r(x,y,w)]$ por:

         $\exists x\forall y[(\exists z \neg (p(x,y)\vee  q(y,z))\vee \exists w r(x,y,w)]$ por:

         $\exists x\forall y[\exists z (\neg p(x,y)\wedge \neg q(y,z))\vee \exists w r(x,y,w)]$ por:

         $[\neg p(A,y)\wedge \neg q(y,f(y))]\vee r(A,y,g(y))$ por:

         $[\neg p(A,y)\vee r(A,y,g(y))]\,\wedge\,[\neg q(y,f(y))\vee r(A,y,g(y))]$

\end{itemize}

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Prova por Resolu\c c\~ao:}

\vspace*{.5cm}
\noindent{\Large Para provar $\alpha$:}

\begin{enumerate} \Large
 \item Negar $\alpha$.
 \item Converter para FNC.
 \item Adicionar \`a BC ( esta na FNC).
 \item Inferir contradi\c c\~ao (cl\'ausula vazia).
\end{enumerate}

\vspace*{.5cm}
\noindent{\Large Exemplos: transpar\^encias 11 e 12.} 

\vfill
\hfill Cap\'{\i}tulo  9: Infer\^encia em L\'ogica de Primeira Ordem

\pagebreak
\noindent {\LARGE\bf Tratamento da Igualdade:}

\vspace*{.5cm}
\begin{itemize} \Large
 \item Regra de {\bf demodula\c c\~ao}:

       \[\frac{t_1=t_2 \,\,\,\,\, [\cdots t_1\cdots]}{[\cdots t_2\sigma\cdots]}\]

       se $\sigma$ \'e umg de $t_1$ e $t_2$.
 \item Regra de {\bf paramodula\c c\~ao}.

\end{itemize}

\vspace*{1cm}
\noindent {\LARGE\bf Estrat\'egias de Resolu\c c\~ao:}

\vspace*{.5cm}
\begin{itemize} \Large
 \item Prefer\^encia pelas unit\'arias.
 \item Conjunto de Suporte.
 \item Resolu\c c\~ao de entrada.
 \item Resolu\c c\~ao linear.
 \item Estrat\'egias de elimina\c c\~ao:
       \begin{itemize}
        \item Cl\'ausulas puras.
        \item Tautologias.
        \item Subjuga\c c\~ao.
       \end{itemize}
\end{itemize}


\end{document}



