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

\hyphenation{ha-bi-li-da-de es-pe-cia-li-za-das e-xem-plo pro-je-to
com-ple-xi-da-de de-sa-pa-re-ce a-bor-da-gem to-ma-da su-ces-so
in-te-li-gen-tes a-gen-te co-nhe-ci-men-to ra-i-nhas e-fei-tos
al-go-rit-mo o-pe-ra-do-res ta-bu-lei-ro co-mo ne-nhu-ma co-lu-na
cons-tan-te E-xem-plos}

\begin{document}

\vspace*{9cm}
\begin{center} \LARGE\bf Cap\'{\i}tulo 7: L\'ogica de Primeira Ordem (LPO)
\end{center}

\vfill
\ 

\pagebreak
\noindent{\Huge\bf Elementos b\'asicos}

\vspace*{1cm}
\noindent{\LARGE\bf Alfabeto:}

\begin{itemize}\Large
 \item Constante: designa um objeto do dom\'{\i}nio. Exemplos:
       2, UFMG, Pel\'e.
 \item S\'{\i}mbolo funcional: designa uma fun\c c\~ao. Exemplos:
       $+$, raiz, m\~ae.
 \item S\'{\i}mbolo predicativo: designa uma rela\c c\~ao.
       Exemplos: $\geq$, irm\~aos, cor.
 \item Vari\'avel (para quantifica\c c\~ao): $x$, $y$, $z$, $a$, $b$, \ldots
 \item Conectivo: $\wedge$, $\vee$, $\neg$, $\Rightarrow$, $\Leftrightarrow$.
 \item Igualdade: $=$
 \item Quantificador: $\forall$, $\exists$.
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\bf Termo:}

\vspace*{.5cm}
\begin{itemize}\Large
 \item Toda constante e toda vari\'avel \'e um termo.
 \item Se $t_1$, $t_2$, \ldots, $t_n$ s\~ao termos e $f$ \'e uma fun\c c\~ao de
       $n$ argumentos, $f(t_1,t_2,\ldots,t_n)$ \'e um termo.
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE Exemplos de termos:}

\begin{itemize}\Large
 \item $x$
 \item UFMG
 \item $\mbox{reitor}(\mbox{UFMG})$
 \item $\mbox{m\~ae}(x)$
 \item $\mbox{m\~ae}(\mbox{reitor}(\mbox{UFMG}))$
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\bf F\'ormula at\^omica:}

\begin{itemize}\Large
 \item Se $t_1$, $t_2$, \ldots, $t_n$ s\~ao termos e $P$ \'e um predicado de
       $n$ argumentos, $P(t_1,t_2,\ldots,t_n)$ \'e uma f\'ormula at\^omica.
 \item Se $t_1$ e $t_2$ s\~ao termos, $t_1=t_2$ \'e uma f\'ormula at\^omica.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Exemplos de f\'ormulas at\^omicas:}

\begin{itemize}\Large
 \item $\mbox{irm\~aos}(\mbox{Abel},\mbox{Caim})$
 \item $\mbox{estuda}(\mbox{m\~ae}(\mbox{reitor}(\mbox{UFMG})),\mbox{UFMG})$
 \item $\mbox{estuda}(x,\mbox{UFMG})$
 \item $\mbox{m\~ae}(\mbox{Abel})=\mbox{m\~ae}(\mbox{Caim})$
 \item $>(\mbox{tam}(\mbox{m\~ae}(\mbox{reitor}(\mbox{UFMG}))),1.70)$
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Senten\c cas complexas:}

\noindent{\Large (esta parte \'e id\^entica \`a de L\'ogica Proposicional)}

\begin{itemize}\Large
 \item Se $S$ \'e uma senten\c ca, $\neg S$ \'e senten\c ca.
 \item Se $S$ \'e uma senten\c ca, $(S)$ \'e senten\c ca.
 \item Se $S_1$ e $S_2$ s\~ao senten\c cas, ent\~ao s\~ao senten\c cas:
       \begin{enumerate}
        \item[\ ] $S_1\wedge S_2$
        \item[\ ] $S_1\vee S_2$
        \item[\ ] $S_1\Rightarrow S_2$
        \item[\ ] $S_1\Leftrightarrow S_2$
       \end{enumerate}
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Alguns exemplos:}

\begin{itemize}\Large
 \item $+(2,2)=4\wedge\mbox{raiz}(4,2)$
 \item $\mbox{ama}(\mbox{m\~ae}(x),x)\vee\neg \mbox{vivo}(x)\vee \neg
         \mbox{vivo}(\mbox{m\~ae}(x))$
 \item $(\mbox{vivo}(x)\wedge\mbox{vivo}(\mbox{m\~ae}(x)))\Rightarrow
        \mbox{ama}(\mbox{m\~ae}(x),x)$
 \item $\mbox{irm\~aos}(\mbox{Abel},\mbox{Caim})\Rightarrow\mbox{irm\~aos}(\mbox{Caim},
        \mbox{Abel})$
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Verdade em LPO}

\vspace*{1cm}
\noindent{\LARGE Uma {\bf interpreta\c c\~ao} para senten\c cas especifica:}
\begin{itemize}\Large
 \item Para cada {\bf constante} um {\em objeto}.
 \item Para cada {\bf s\'{\i}mbolo funcional} uma {\em fun\c c\~ao}.
 \item Para cada {\bf s\'{\i}mbolo predicativo} uma {\em rela\c c\~ao}.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Interpretando senten\c cas at\^omicas:}

\begin{center}\Large
\begin{tabular}{ll}
Senten\c ca & Interpreta\c c\~ao \\ \hline
$+(2,2)=4$ & $2+2$ e $4$ referem-se ao mesmo objeto \\
$\mbox{m\~ae}(\mbox{Eva},\mbox{Abel})$ & $(\mbox{\em Eva},\mbox{\em Abel})\in
 \mbox{\em m\~ae-de}$ \\
\end{tabular}
\end{center}

\vspace*{1cm}
\noindent{\LARGE Os conectivos s\~ao interpretados como em L\'ogica Proposicional.}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Quantificador universal}

\begin{itemize}\Large
 \item Se $S$ \'e uma senten\c ca, $\forall x,y,\ldots S$ \'e senten\c ca.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Alguns exemplos:}

\begin{itemize}\Large
 \item $\forall x (\mbox{homem}(x)\Rightarrow\mbox{mortal}(x))$
 \item $\forall x[(\mbox{vivo}(x)\wedge\mbox{vivo}(\mbox{m\~ae}(x)))\Rightarrow
        \mbox{ama}(\mbox{m\~ae}(x),x)]$
 \item $\forall x,y(\mbox{irm\~aos}(x,y)\Rightarrow\mbox{irm\~aos}(y,x))$
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\bf Significado da quantifica\c c\~ao universal:}

\vspace*{.5cm}
\begin{itemize}\Large
 \item $\forall x S$ equivale \`a {\em conjun\c c\~ao} de {\em instancia\c c\~oes\/} de
        $S$.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Exemplo: $\forall x (\mbox{homem}(x)\Rightarrow\mbox{mortal}(x))$}

\hspace*{2.5cm}{\LARGE significa o mesmo que:}

\begin{enumerate} \Large
 \item[\ ] \hspace*{4mm}$(\mbox{homem}(\mbox{S\'ocrates})\Rightarrow\mbox{mortal}(\mbox{S\'ocrates}))$
 \item[\ ] $\wedge(\mbox{homem}(\mbox{Plat\~ao})\Rightarrow\mbox{mortal}(\mbox{Plat\~ao}))$
 \item[\ ] $\wedge(\mbox{homem}(\mbox{Zeno})\Rightarrow\mbox{mortal}(\mbox{Zeno}))$
 \item[\ ] $\wedge \cdots$
\end{enumerate}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\pagebreak
\noindent{\LARGE\bf Quantificador existencial}

\begin{itemize}\Large
 \item Se $S$ \'e uma senten\c ca, $\exists x,y,\ldots S$ \'e senten\c ca.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Alguns exemplos:}

\begin{itemize}\Large
 \item $\exists x (\mbox{animal}(x)\wedge\mbox{racional}(x))$
 \item $\exists x [\mbox{gosta}(x,\mbox{Maria})\wedge\neg\mbox{gosta}(x,
            \mbox{m\~ae}(\mbox{Maria}))]$
 \item $\exists x,y(\mbox{irm\~aos}(x,y)\wedge\mbox{gosta}(x,y))$
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\bf Significado da quantifica\c c\~ao existencial:}

\vspace*{.5cm}
\begin{itemize}\Large
 \item $\exists x S$ equivale \`a {\em disjun\c c\~ao} de {\em instancia\c c\~oes\/} de
        $S$.
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE Exemplo: $\exists x (\mbox{animal}(x)\wedge\mbox{racional}(x))$}

\hspace*{2.5cm}{\LARGE significa o mesmo que:}

\begin{enumerate} \Large
 \item[\ ] \hspace*{4mm}$(\mbox{animal}(\mbox{S\'ocrates})\wedge\mbox{racional}(\mbox{S\'ocrates}))$
 \item[\ ] $\vee(\mbox{animal}(\mbox{Plat\~ao})\wedge\mbox{racional}(\mbox{Plat\~ao}))$
 \item[\ ] $\vee(\mbox{animal}(\mbox{Zeno})\wedge\mbox{racional}(\mbox{Zeno}))$
 \item[\ ] $\vee \cdots$
\end{enumerate}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE Tipicamente, quando se usa $\forall$ o conectivo principal \'e $\Rightarrow$:}

\begin{itemize}\Large
 \item {\em Todo c\~ao \'e mam\'{\i}fero\/}:
       \begin{enumerate}
        \item[\ ] $\forall x (\mbox{c\~ao}(x)\Rightarrow\mbox{mam\'{\i}fero}(x))$
       \end{enumerate}
 \item {\em O homem \'e um animal racional\/}:
       \begin{enumerate}
        \item[\ ] $\forall x [\mbox{homem}(x)\Rightarrow(\mbox{animal}(x)\wedge
                 \mbox{racional}(x))]$
       \end{enumerate}
 \item {\em Os irm\~aos de Pedro moram em Belo Horizonte\/}:
       \begin{enumerate}
        \item[\ ] $\forall x (\mbox{irm\~aos}(\mbox{Pedro},x)\Rightarrow\mbox{mora}(x,
                  \mbox{BH}))$
       \end{enumerate}
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE Tipicamente, quando se usa $\exists$ o conectivo principal \'e $\wedge$:}

\begin{itemize}\Large
 \item {\em Existem homens irracionais\/}:
       \begin{enumerate}
        \item[\ ] $\exists x (\mbox{homem}(x)\wedge\neg\mbox{racional}(x))$
       \end{enumerate}
 \item {\em Alguns alunos gostam de L\'ogica\/}:
       \begin{enumerate}
        \item[\ ] $\exists x [\mbox{aluno}(x)\wedge\mbox{gosta}(x,\mbox{L\'ogica})]$
       \end{enumerate}
 \item {\em Algu\'em temido por todos detesta L\'ogica\/}:
       \begin{enumerate}
        \item[\ ] $\exists x (\forall y\,\mbox{teme}(y,x)\wedge\mbox{odeia}(x,\mbox{L\'ogica}))$
       \end{enumerate}
\end{itemize}


\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Propriedades dos quantificadores}

\vspace*{1cm}
\begin{itemize} \Large
 \item $\forall x\forall y S\equiv\forall y\forall x S$
 \item $\exists x\exists y S\equiv\exists y\exists x S$
 \item $\exists x\forall y S\not\equiv\forall y\exists x S$
       \begin{enumerate}
        \item[\ ] $\exists x\forall y\, \mbox{ama}(x,y)$

                  ({\em Algu\'em ama todo mundo.})
        \item[\ ] $\forall y\exists x\, \mbox{ama}(x,y)$

                  ({\em Todo mundo \'e amado por algu\'em.})
       \end{enumerate}
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\bf Leis de De Morgan para senten\c cas quantificadas e n\~ao
quantificadas:}

\begin{center} \Large
\begin{tabular}{rclcrcl}
 $\neg \forall x S$&$\equiv$&$\exists x\neg S$& \ \ \ &$\neg(S_1\wedge S_2)$&$\equiv$&
  $\neg S_1\vee \neg S_2$ \\
 $\neg \exists x S$&$\equiv$&$\forall x\neg S$& \ \ \ &$\neg(S_1\vee S_2)$&$\equiv$&
  $\neg S_1\wedge \neg S_2$ \\
 $\forall x S$&$\equiv$&$\neg\exists x\neg S$& \ \ \ &$S_1\wedge S_2$&$\equiv$&
  $\neg(\neg S_1\vee\neg S_2)$ \\
 $\exists x S$&$\equiv$&$\neg\forall x\neg S$& \ \ \ &$S_1\vee S_2$&$\equiv$&
  $\neg(\neg S_1\wedge\neg S_2)$
\end{tabular}
\end{center}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Igualdade}

\vspace*{1cm}
\noindent {\Large $t_1=t_2$ \'e verdadeiro sob uma interpreta\c c\~ao}

\vspace*{.3cm}
\noindent {\Large se, e somente se}

\vspace*{.3cm}
\noindent {\Large  $t_1$ e $t_2$ referem-se ao mesmo objeto.}

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

\begin{itemize} \Large
 \item $1=2$ \'e satisfat\'{\i}vel.
 \item $\forall x \times(\mbox{raiz}(x),\mbox{raiz}(x))=x$ \'e satisfat\'{\i}vel.
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE Exemplos de uso da igualdade:}

\begin{itemize} \Large
 \item Ana ama uma \'unica pessoa:
      \begin{enumerate}
       \item[\ ] $\exists x[\mbox{ama}(\mbox{Ana},x)\wedge\forall y(\mbox{ama}(\mbox{Ana},y)
                 \Rightarrow x=y)]$
      \end{enumerate}
 \item Jos\'e ama no m\'{\i}nimo 2 pessoas:
      \begin{enumerate}
       \item[\ ] $\exists x,y[\mbox{ama}(\mbox{Jos\'e},x)\wedge\mbox{ama}(\mbox{Jos\'e},y)\wedge
                  \neg(x=y)]$
      \end{enumerate}
 \item Defini\c c\~ao da rela\c c\~ao ``irm\~aos'':
      \begin{enumerate}
       \item[\ ] $\forall x,y\{\mbox{irm\~aos}(x,y)\Leftrightarrow \neg (x=y)\wedge$
       \item[\ ] \hspace*{1cm}$\exists m,p [\neg(m=p)\wedge\mbox{pai}(p,x)\wedge\mbox{m\~ae}(m,x)\wedge$
      \item[\ ] \hspace*{2cm}$\mbox{pai}(p,y)\wedge\mbox{m\~ae}(m,y)]\}$
     \end{enumerate}
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Interagindo com uma BC}

\vspace*{1cm}
\noindent {\LARGE Introduzindo senten\c cas:}

\begin{enumerate} \Large
 \item[\ ] $\mbox{TELL}(\mbox{BC},\forall x,y[\mbox{m\~ae}(x)=y\Leftrightarrow \mbox{fem}(x)
            \wedge \mbox{filh}(y,x)])$
 \item[\ ] $\mbox{TELL}(\mbox{BC},\mbox{fem}(\mbox{Ana})\wedge\mbox{filh}(\mbox{Leo},\mbox{Ana})
            \wedge \mbox{filh}(\mbox{Sue},\mbox{Leo}))$
 \item[\ ] $\cdots$
\end{enumerate}

\vspace*{.5cm}
\noindent {\LARGE Consultando a BC:}

\begin{enumerate} \Large
 \item[\ ] $\mbox{ASK}(\mbox{BC},\mbox{av\'o}(\mbox{Ana},\mbox{Sue}))$

           \hspace*{1cm}Resp: {\em sim}.
 \item[\ ] $\mbox{ASK}(\mbox{BC},\mbox{av\'o}(\mbox{Ana},x))$

           \hspace*{1cm}Resp: {\em sim}, $x/\mbox{Sue}$ \hspace*{.5cm} $\leftarrow$ 
           {\bf substitui\c c\~ao}
 \item[\ ] $\cdots$
\end{enumerate}

\vspace*{.5cm}
\noindent {\Large $S\sigma$: resultado de aplicar a substitui\c c\~ao $\sigma$ na
senten\c ca $S$.}

\vspace*{.3cm}
\noindent {\Large Exemplo:}

\begin{itemize} \Large
 \item Sendo $S=\mbox{irm\~aos}(x,y)$ e $\sigma=\{x/\mbox{Abel},y/\mbox{Caim}\}$:

       \hspace*{.5cm} $S\sigma=\mbox{irm\~aos}(\mbox{Abel},\mbox{Caim})$
\end{itemize}

\vspace*{.5cm}
\noindent {\Large $\mbox{ASK}(\mbox{BC},S)$ retorna $\sigma$ tal que $S\sigma$
(algum, todos?).}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\Huge\bf Agentes l\'ogicos para o mundo do Wumpu}

\vspace*{1cm}
\noindent{\LARGE\bf Um agente Baseado em Conhecimento gen\'erico:}

\vspace*{2.5cm}
\begin{center}
Figura 7.2
\end{center}

\vspace*{2.5cm}
\noindent{\Large $\mbox{\large MAKE-PERCEPT-SENTENCE}(\mbox{percept},5)$ produz:}

\begin{itemize} \Large
 \item $\mbox{est}([\mbox{cheiro},\mbox{brisa},\mbox{brilho},-,-],5)$
\end{itemize}

\vspace*{.5cm}
\noindent{\Large A\c c\~oes poss\'{\i}veis para o agente:}

\begin{itemize} \Large\em
 \item $\mbox{vire}(\mbox{esq})$, $\mbox{vire}(\mbox{dir})$, anda, pega, larga, atira, sai.
\end{itemize}

\vspace*{.5cm}
\noindent{\Large $\mbox{\large MAKE-ACTION-QUERY}(5)$ produz:}

\begin{itemize} \Large
 \item $\mbox{a\c c\~ao}(a,5)$
\end{itemize}

\vspace*{.5cm}
\noindent{\Large \mbox{\large ASK} retorna substitui\c c\~ao do tipo $\{a/\mbox{\em atira}\}$}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\Huge\bf Agente do tipo reflexo}

\vspace*{1cm}
\noindent{\LARGE\bf Percep\c c\~ao:}

\begin{itemize}\Large
 \item $\forall v,b,z,g,t\,[\mbox{est}([\mbox{cheiro},v,b,z,g],t)\Rightarrow
        \mbox{cheirou}(t)]$
 \item $\forall c,b,z,g,t\,[\mbox{est}([c,\mbox{brisa},b,z,g],t)\Rightarrow
        \mbox{brisa}(t)]$
 \item $\forall c,v,z,g,t\,[\mbox{est}([c,v,\mbox{brilho},z,g],t)\Rightarrow
        \mbox{no-ouro}(t)]$
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE\bf Indicando a a\c c\~ao (reflexo):}

\begin{itemize}\Large
 \item $\forall t\,[\mbox{no-ouro}(t)\Rightarrow \mbox{a\c c\~ao}(\mbox{\em pega},t)]$
\end{itemize}

\vspace*{.5cm}
\noindent{\LARGE\bf Problema:}

\begin{itemize}\Large
 \item {\bf Agente n\~ao tem mem\'oria (estado) interna.}
 \item Exemplo: como saber se j\'a est\'a com o ouro?
       \begin{enumerate}
        \item[\ ] $\forall t[\mbox{no-ouro}(t)\wedge\neg \mbox{com}(\mbox{ouro},t)\Rightarrow
                   \mbox{a\c c\~ao}(\mbox{\em pega},t)]$
        \item[\ ] $\mbox{com}(\mbox{ouro},t)$ n\~ao pode ser \underline{observado} pelo agente!
        \item[\ ] $\Rightarrow$ Necess\'ario anotar {\em mudan\c cas\/} no mundo.
       \end{enumerate}
 \item Outro exemplo: agente n\~ao sabe em qual local est\'a; como saber quando sair?
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\Huge\bf Anotando mudan\c cas no mundo}

\vspace*{1cm}
\noindent{\LARGE\bf C\'alculo das situa\c c\~oes:}

\vspace*{.5cm}
\begin{enumerate}\Large
 \item[\ ] Um argumento em cada predicado representa a {\em situa\-\c c\~ao\/} em que ele se
           aplica, a menos que ele se aplique a toda situa\c c\~ao.
 \item[\ ] Exemplo: ao inv\'es de $\mbox{local}(\mbox{Agente},[i,j])$, diz-se:
           \begin{itemize}
            \item $\mbox{local}(\mbox{Agente},[1,1],S_0)\wedge\mbox{local}(\mbox{Agente},[1,2],S_1)$,
                  \ldots
           \end{itemize}
\end{enumerate}

\vspace*{1cm}
\begin{flushleft} \large
$\mbox{Res}(\mbox{\em anda},S_0)=S_1$ \\
$\mbox{Res}(\mbox{\em vira}(\mbox{\em dir}),S_1)=S_2$ \\
$\mbox{Res}(\mbox{\em anda},S_2)=S_3$ \\
\end{flushleft}

\vspace*{1.5cm}
\begin{center}
Figura 7.3
\end{center}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf C\'alculo das situa\c c\~oes/Axiomas:}

\vspace*{1cm}
\noindent{\LARGE Axiomas de \underline{efeito}:} {\LARGE o que {\bf muda} ap\'os a\c c\~ao}

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

\begin{itemize}\Large
 \item $\forall s[\mbox{no-ouro}(s)\Rightarrow
        \mbox{com}(\mbox{ouro},\mbox{Res}(\mbox{\em pega},s))]$
 \item $\forall s,x\,\neg\mbox{com}(x,\mbox{Res}(\mbox{\em larga},s))$
\end{itemize}

\vspace*{1cm}
\noindent{\LARGE\em \underline{Frame} axioms:} {\LARGE o que {\bf n\~ao muda} ap\'os a\c c\~ao}

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

\begin{itemize}\Large
 \item $\forall s[\mbox{tem-flexa}(s)\Rightarrow
        \mbox{tem-flexa}(\mbox{Res}(\mbox{\em pega},s))]$
 \item $\forall s\,\mbox{tem-flexa}(\mbox{Res}(\mbox{\em larga},s))]$
 \item $\forall a,x,s[\mbox{com}(x,s)\wedge(a\not= \mbox{\em larga})\Rightarrow
        \mbox{com}(x,\mbox{Res}(a,s))]$
 \item $\forall a,x,s[\neg\mbox{com}(x,s)\wedge(a\not= \mbox{\em pega}\vee\neg\mbox{presente}(x,s))
        \Rightarrow\neg \mbox{com}(x,\mbox{Res}(a,s))]$
\end{itemize}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Frame problem:} {\LARGE como lidar com a ``n\~ao mudan\c ca''?}

\begin{enumerate} \Large
 \item[(a)] {\em Representa\c c\~ao:} evitar {\em frame axioms}.
 \item[(a)] {\em Infer\^encia:} evitar re-inferir fatos que n\~ao mudam.
\end{enumerate}

\vspace*{.5cm}
\noindent{\LARGE Resolvendo o {\em frame problem\/} representacional: \underline{axiomas
 de estado-sucessor}} 

\begin{enumerate} \Large
 \item[\ ] $\Rightarrow$ Um axioma mostrando todas as formas do pre\-di\-ca\-do ficar verdadeiro 
           \underline{no pr\'oximo estado} e todas as formas dele ficar falso:
 \item[\ ]\begin{tabular}{ccl}
           $P$ verdadeiro ap\'os&$\Leftrightarrow$&a\c c\~ao faz $P$ verdadeiro \\
           & & $\vee$ $P$ j\'a verdadeiro\\
           & & e nenhuma a\c c\~ao o faz falso
          \end{tabular}
 \item[\ ] Exemplo:

          $\forall a,x,s\,\mbox{com}(x,\mbox{Res}(a,s))\Leftrightarrow [(a=\mbox{\em pega}\wedge
           \mbox{presente}(x,s))\vee(\mbox{com}(x,s)\wedge a\not=\mbox{\em larga}) ]$
\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE $\Rightarrow$ Um axioma para cada predicado que pode se modificar no tempo.}

\vfill
\hfill L\'ogica de Primeira Ordem

\pagebreak
\noindent{\LARGE\bf Lidando com a localiza\c c\~ao}

\vspace*{1cm}
\begin{itemize}\Large
 \item Local inicial: $\mbox{local}(\mbox{Agente},[1,1],S_0)$.

 \item Dire\c c\~ao: $\mbox{Orient}(\mbox{Agente},S_0)=0$.

 \item Local em frente dada uma dire\c c\~ao (em graus):
       \begin{enumerate}
        \item[\ ] $\forall x,y\, \mbox{loc-f}([x,y],0)=[x+1,y]$
        \item[\ ] $\forall x,y\, \mbox{loc-f}([x,y],90)=[x,y+1]$
        \item[\ ] $\forall x,y\, \mbox{loc-f}([x,y],180)=[x-1,y]$
        \item[\ ] $\forall x,y\, \mbox{loc-f}([x,y],270)=[x,y-1]$
       \end{enumerate}

       Local em frente do agente $p$ que est\'a em $l$:
       \begin{enumerate}
        \item[\ ] $\forall p,l,s\, \mbox{local}(p,l,s)\Rightarrow$ \\
                  \hspace*{2cm}$\mbox{loc-a-f}(p,s)=\mbox{loc-f}(l,\mbox{Orient}(p,s))$
       \end{enumerate}

       Adjac\^encia:
       \begin{enumerate}
        \item[\ ] $\forall l_1,l_2\, \mbox{adj}(l_1,l_2)\Leftrightarrow\exists
                    d\, l_1=\mbox{loc-f}(l_2,d)$
       \end{enumerate}

 \item Detalhes geogr\'aficos do mapa:
       \begin{enumerate}
        \item[\ ] $\forall x,y\, \mbox{parede}([x,y])\Leftrightarrow$ \\
                   \hspace*{2cm}$(x=0\vee x=5\vee y=0\vee y=5)$
       \end{enumerate}

\vfill
\hfill {\normalsize L\'ogica de Primeira Ordem}

\pagebreak
 \item Influ\^encia das a\c c\~oes: apenas {\em anda\/} influencia.
       \begin{enumerate}
        \item[\ ] $\forall a,l,p,s\, \mbox{local}(p,l,\mbox{Res}(a,s))\Leftrightarrow$ \\
                   \hspace*{2cm}$(a=\mbox{\em anda}\wedge l=\mbox{loc-a-f}(p,s)\wedge
                                 \neg\mbox{parede}(l))$ \\
                   \hspace*{2cm}$\vee(\mbox{local}(p,l,s)\wedge a\not=\mbox{\em anda})$
       \end{enumerate}

 \item Influ\^encia das a\c c\~oes na dire\c c\~ao:
       \begin{enumerate}
        \item[\ ] $\forall a,d,p,s\, \mbox{Orient}(p,\mbox{Res}(a,s))=d\Leftrightarrow$ \\
                   $(a=\mbox{\em vira}(\mbox{\em dir})\wedge d=
                                 \mbox{\em mod}(\mbox{Orient}(p,s)-90,360))$ \\
                   $\vee(a=\mbox{\em vira}(\mbox{\em esq})\wedge d=
                                 \mbox{\em mod}(\mbox{Orient}(p,s)+90,360))$ \\
                   $\vee(\mbox{Orient}(p,s)=d\wedge
                                 \neg(a=\mbox{\em vira}(\mbox{\em dir})\vee
                                      a=\mbox{\em vira}(\mbox{\em esq})))$
       \end{enumerate}
\end{itemize}

\vfill
\hfill {\normalsize L\'ogica de Primeira Ordem}

\pagebreak
\noindent{\Huge\bf Deduzindo propriedades ``ocultas''}

\vspace*{1cm}
\noindent {\LARGE Propriedades dos locais:}

\begin{enumerate} \Large
 \item $\forall l, s [\mbox{local}(\mbox{Agente},l,s)\wedge\mbox{brisa}(s)\Rightarrow
        \mbox{ventando}(l)]$
 \item $\forall l, s [\mbox{local}(\mbox{Agente},l,s)\wedge\mbox{cheiro}(s)\Rightarrow
        \mbox{cheirando}(l)]$
\end{enumerate}

\vspace*{1cm}
\noindent{\LARGE $\Rightarrow$ ``Est\'a ventando perto dos buracos'':}

\vspace*{.5cm}
\noindent {\LARGE Regra de {\bf diagn\'ostico}: infere causa a partir do efeito}

\begin{enumerate} \Large
 \item $\forall l [\mbox{ventando}(l)\Rightarrow\exists l_1 \mbox{buraco}(l_1)\wedge
        \mbox{adj}(l,l_1)]$
\end{enumerate}

\vspace*{.5cm}
\noindent {\LARGE Regra {\bf causal}: infere efeito a partir da causa}

\begin{enumerate} \Large
 \item $\forall l,l_1 [\mbox{buraco}(l)\wedge\mbox{adj}(l,l_1)\Rightarrow
        \mbox{ventando}(l_1)]$
\end{enumerate}

\vspace*{1cm}
\noindent{\LARGE{\bf Defini\c c\~ao} de ``ventando'':}

\begin{enumerate} \Large
 \item $\forall l [\mbox{ventando}(l)\Leftrightarrow\exists l_1 \mbox{buraco}(l_1)\wedge
        \mbox{adj}(l,l_1)]$
\end{enumerate}

\vspace*{1cm}
\noindent{\LARGE{\bf Defini\c c\~ao} de ``OK'':}

\begin{enumerate} \Large
 \item $\forall l,s [\mbox{OK}(l)\Leftrightarrow \neg\mbox{buraco}(l)\wedge\neg
        \mbox{local}(\mbox{Wumpu},l,s)]$
\end{enumerate}

\vfill
\hfill {\normalsize L\'ogica de Primeira Ordem}

\pagebreak
\noindent{\Huge\bf Fazendo planos}

\vspace*{1cm}
\noindent {\LARGE Condi\c c\~ao inicial em BC:}

\begin{enumerate}\Large
 \item[\ ] $\mbox{local}(\mbox{Agente},[1,1],S_0)$
 \item[\ ] $\mbox{local}(\mbox{Ouro},[1,2],S_0)$
\end{enumerate}

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

\begin{enumerate}\Large
 \item[\ ] $\mbox{\large ASK}(\mbox{\large BC},\mbox{com}(\mbox{Ouro},s))$
 \item[\ ] {\em (Em que situa\c c\~ao estarei com o ouro?)}
\end{enumerate}

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

\begin{enumerate}\Large
 \item[\ ] $\{s/\mbox{Res}(\mbox{\em pega},\mbox{Res}(\mbox{\em anda},S_0))\}$
 \item[\ ] {\em (Anda e depois pega o ouro.)}
\end{enumerate}

\vfill
\hfill {\normalsize L\'ogica de Primeira Ordem}

\pagebreak
\noindent {\LARGE\bf Uma outra forma para planos:}

\begin{itemize}\Large
 \item Sequ\^encia de a\c c\~oes: $[a_1,a_2,\ldots,a_n]$.
\end{itemize}

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

\begin{enumerate}\Large
 \item[\ ] $\mbox{\large ASK}(\mbox{\large BC},\mbox{com}(\mbox{Ouro},\mbox{plano}(p,S_0)))$
 \item[\ ] {\em (Me d\^e um plano para conseguir o ouro a partir de $S_0$.)}
\end{enumerate}

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

\begin{enumerate}\Large
 \item[\ ] $\{p/[\mbox{\em anda},\mbox{\em pega}]\}$
 \item[\ ] {\em (Anda e depois pega o ouro.)}
\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE Defini\c c\~ao de plano em termos de Res:}

\begin{enumerate}\Large
 \item[\ ] $\forall s\,\, \mbox{plano}([],s)=s$
 \item[\ ] $\forall a,p,s\,\, \mbox{plano}([a|p],s)=\mbox{plano}(p,\mbox{Res}(a,s))$
\end{enumerate}

\vspace*{1cm}
\noindent {\LARGE Sistemas de {\bf planejamento}: sistemas de prop\'osito espec\'{\i}fico para
este tipo de infer\^encia.}

\vfill
\hfill {\normalsize L\'ogica de Primeira Ordem}

\end{document}
