%\documentclass[dvips,12pt]{amsart}
\documentclass[pdftex,12pt]{amsart}
\usepackage{amsmath}
\usepackage[portuges]{babel}
\usepackage{enumerate}

\usepackage{hyperref}
\def\hbref#1#2#3{\href{#1#2}{#3}}

\def\crseurl{http://www.inf.ufes.br/~raulh/ufes/teaching/courses/lpii}

\def\cwurl{\crseurl/page/cw/0/}

\def\inmacros#1{\input{$HOME/tex/macros/#1}}

\inmacros{defport}

\def\stb#1#2{\ensuremath{st.#1.b.#2}}
\def\xstb#1#2#3{\ensuremath{\stb#1#2=\langle#3\rangle}}
\def\xoldstb#1#2#3{\ensuremath{#1\in\stb#2#3}}

\def\stdin{\emph{stdin}}
\def\stdout{\emph{stdout}}
\def\tarball{\emph{tarball}}
\def\mailto#1{\href{mailto:#1}{#1}}
\title{Trabalho 0 \\ Intelig\^encia Artificial}

\author{Raul H.C. Lopes}
\def\radixsort{\emph{radix sort}}
\def\splitter{\emph{splitter}}
\def\quicksort{\emph{quick sort}}
\def\mergesort{\emph{merge sort}}
\def\prefsum{prefix sum}
\def\real{Real}


\def\scref#1{sc. \ref{#1}}
\def\exref#1{ex. \ref{ex:#1}}
\def\tabref#1{tab. \ref{tab:#1}}

\begin{document}

\maketitle

\section{Preliminares}
Este trabalho demanda a resolu\c{c}\~ao de pequenos exerc\'{\i}cios de
implementa\c{c}\~ao, abordando os t\'opicos de busca e resolu\c{c}\~ao de
problemas usando l\'ogica. Nesses exerc\'{\i}cios, use as seguintes ferramentas:
\def\prolog{\emph{Prolog}}
\def\lisp{\emph{Lisp}}
\def\prover{\emph{Provador}}
\def\inet{\emph{Internet}}
\begin{itemize}
	\item \prolog: \emph{teyjus} lambda prolog, \emph{Yap} prolog, 
		ou \emph{SWI} prolog.
	\item \lisp: \emph{CMU/SBCL} Common Lisp, \emph{chicken} scheme, ou
		\emph{DrScheme}.
	\item \prover: um dentre \emph{Otter, Isabelle, Phox, Twelf, Spass.}
\end{itemize}

Note que para v\'arios dos exerc\'{\i}cios existem solu\c{c}\~oes propostas
na \inet. Mas, seu objetivo consiste em apresentar as solu\c{c}\~oes obtidas
pelos seus programas.

O trabalho pode ser resolvido em dupla.

\section{M\'aquina Turing}
\def\ndtm{\textbf{NDTM}}
\def\Halt{\ensuremath{\mathcal{H}}}
\def\Yes{\ensuremath{\mathcal{Y}}}
\def\No{\ensuremath{\mathcal{N}}}
\def\finalst{\ensuremath{\{\Halt,\Yes,\No\}}}
\def\Skip{\ensuremath{--}}
\def\Left{\ensuremath{\leftarrow}}
\def\Right{\ensuremath{\rightarrow}}
\def\moves{\ensuremath\{\Skip,\Left,\Right\}}
\def\strin{\emph{string}}

\begin{qst}
	Implemente em l\'ogica (\prover\ ou \prolog) \ e em \lisp, simuladores para execu\c c\~ao de 
	programas de m\'aquina de Turing n\~ao determin\'{\i}stica, \ndtm.

	Uma \ndtm\ \'e uma tupla $(K,\Sigma,\Delta,s)$, onde:
	\begin{itemize}
		\item $K$ \'e um conjunto de estados.
		\item $\Sigma$ \'e o alfabeto de s\'{\i}mbolos lidos/escritos por
			sua m\'aquina.
		\item $K\cap(\Sigma\cup\finalst = \empty$.
		\item $\finalst\not\subset\Sigma$.
		\item \Halt\ ser\'a usado para estado final de computa\c c\~ao.
		\item \Yes\ \'e usado para estado final de aceita\c c\~ao do \strin\
			de entrada.
		\item \No\ \'e usado para estado final de rejei\c c\~ao do 
			\strin\ de entrada.
		\item \moves\ indicam respetivamente aus\^encia de movimento, movimento
			para a esquerda e para a direita da cabe\c ca de leitura.
		\item $\moves\cap\Sigma=\empty\land\moves\cap K=\empty$.
		\item $\Delta\subset (K \times \Sigma) \times
			[(K\cup\finalst)\times\Sigma\times\moves]$
	\end{itemize}
	
	
	Sua m\'aquina poder\'a opcionalmente ter mais de uma fita. Ela poder\'a
	ser usada para dois tipos de computa\c c\~ao:
	\begin{itemize}
		\item c\'alculo de fun\c coes, quando a m\'aquina, se parar, terminar\'a 
			em estado \Halt.
		\item reconhecimento de \strin s, quando ela pode parar em \Yes,
			\strin\ aceito, ou \No, recusado. Note que uma \ndtm\ s\'o recusa
			um \strin\ se todas as transi\c c\~oes poss\'{\i}veis terminam em
			\No.
	\end{itemize}

	Seu simulador ser\'a o \emph{hardware} de execu\c c\~ao de programas
	gerais de \ndtm. Assuma que:

	\begin{itemize}
		\item inicialmente, seu simulador receber\'a:
			\begin{itemize}
				\item a rela\c c\~ao de transi\c c\~ao da m\'aquina como
					uma lista de tuplas;
				\item o conte\'udo inicial da fita.
			\end{itemize}
		\item seu simulador retornar\'a o resultado da computa\c c\~ao: 
			estado final e conte\'udo da fita.
	\end{itemize}

\end{qst}

\section{Puzzles}
\def\utopia{\emph{Utopia}}
\begin{qst}
	Na ilha de \utopia, n\~ao existe crime maior do que a pregui\c{c}a e 
	o primeiro sintoma dessa doen\c{c}a \'e uma estranha marca branca que
	aparece na testa do pregui\c{c}oso. Um estudante passeando pelas ruas
	encontra tr\^es senadores e comunica-lhes que, ao menos um, tem uma
	marca de pregui\c{c}a na testa. O primeiro senador reage dizendo:
	``eu n\~ao sei se tenho ou n\~ao uma mancha na testa.'' O terceiro
	senador, o \'unico minimamente inteligente, diz: ``Eu sei que tenho uma
	mancha branca na testa e posso provar.'' Note que l\'a como c\'a
	senadores em geral s\~ao pregui\c cosos, embora eles acreditem que 
	aparentam o oposto.

	Formalize essa hist\'oria em um provador e encontre a suposta prova do
	terceiro senador.

	\textsl{Considere o que se pode concluir da fala do primeiro senador.
	Raciocine sobre o que conhecimento que cada um tem do conhecimento dos
	outros.}
\end{qst}

\def\goedel{G\"odel}
\def\brlan{\emph{Brasil\^andia}}
\begin{qst}
	% 035
	Em \brlan, existem dois tipos de pessoas: senadores, que sempre mentem,
	e idiotas, que sempre dizem a verdade. \goedel\ foi passear em \brlan,
	encontrou dois cidad\~aos $X$ e $Y$ e perguntou a $X$: ``algum de voc\^es 
	\'e um idiota?'' 

	Formalize essa hist\'oria em um provador e use-o para obter o que 
	\goedel\ pode concluir a partir das poss\'{\i}veis respostas que ele
	pode ter ouvido.
\end{qst}

\def\A{$A$}
\def\B{$B$}
\def\C{$C$}
\begin{qst}
	%23 
	Continuando em \brlan, \goedel\ encontra com tr\^es cidad\~aos:
	\A, \B, e \C. Ele pergunta a \A: ``Quantos idiotas h\'a entre voc\^es?''
	\A\ resmunga uma resposta inintelig\'{\i}vel, caracter\'{\i}stica do
	funcionalismo do local. \goedel\ pergunta a \B:``O que 
	\A\ disse?'' \B\ responde: ``\A\ disse que existe exatamente um idiota 
	entre n\'os.'' Mas, \C\ interfere e diz: ``N\~ao acredite em \B!''. 

	Use seu provador para ajudar \goedel\ a resolver o enigma.

	\textsl{Dica: se sua formaliza\c c\~ao for consistente e \goedel\ for
	sortudo, existe uma resposta.}
\end{qst}

\def\shaved{\emph{limpou}}

\def\X{$X$}
\def\Y{$Y$}

\begin{qst}
	%003
	Existe um clube de safados onde imperam as seguintes leis:
	\begin{itemize}
		\item Se um safado \X\ do clube \shaved\ um outro safado \Y\
			do clube, ent\~ao todos os membros do clube j\'a \shaved\ \X.
		\item Roberto, Lula, FFHH e Dirceu pertencem ao clube.
		\item Roberto \shaved\ Dirceu.
	\end{itemize}
	Prove que FFHH \shaved\ Lula.

\end{qst}

\section{L\'ogica}

\begin{qst}\label{ex:drinker}
	Use um provador para provar que ``em qualquer boteco, existe uma pessoa
	tal que se ela bebe, ent\~ao todo mundo bebe.''
\end{qst}

\begin{qst}
	Tente resolver o \exref{drinker}, usando l\'ogica construtiva. 
\end{qst}

\end{document}

