%\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}
\inmacros{deflogic}
\inmacros{defseqs}
\title{Teoria da Computa\c{c}\~ao\\ Prova de Teoremas}


\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}}
\def\stdin{\emph{stdin}}

\begin{document}

\maketitle

\section{Introdu\c{c}\~ao}
Este exerc\'{\i}cio \'e estritamente individual. Cada aluno usr\'a um provador
diferente. O objetivo maior do exerc\'{\i}cio consiste em  treinar seu 
conhecimento de prova.

\section{L\'ogica de primeira ordem}
\begin{ex}
	Para cada um dos exerc\'{\i}cios a seguir fa\c{c}a, se poss\'{\i}vel:
	\begin{itemize}
		\item Construa uma prova usando seu provador, em modo
			autom\'atico.
		\item Construa uma prova usando seu provador, evitando passos
			autom\'aticos.
		\item Justifique informalmente cada passo da segunda prova.
	\end{itemize}

	Os exerc\'{\i}cios:
	\begin{enumerate}
		\item $p \limp (q \limp p)$
		\item $p \limp (q \limp p \land q)$
		\item $(p \limp q) \limp (p \land r \llr.\limp q\land r)$
		\item $(p \limp \lnot p)\limp \lnot p$
		\item $\pand p{\lnot q} \llr.\limp \lnot\ppimp pq$
		\item $\ppimp pq \land \ppimp p{\lnot q} \llr.\limp \lnot p$
		\item $\forall x:\exists y: p(x) \limp p(y)$
		\item $\exists x:\forall y: p(x) \limp q(y)$
		\item $\forall x: (p(x) \land q(x)) \limp  
			(\forall x: p(x) \land  \forall x: q(x))$
	\end{enumerate}
\end{ex}

\section{Seq\"u\^encias}


\begin{ex} 
	Formalize o conceito de seq\"u\^encias e resolva os exerc\'{\i}cios.
	Para cada um dos exerc\'{\i}cios a seguir fa\c{c}a:
	\begin{itemize}
		\item Construa uma prova usando seu provador, em modo
			autom\'atico.
		\item Construa uma prova usando seu provador, evitando passos
			autom\'aticos.
		\item Justifique informalmente cada passo da segunda prova.
	\end{itemize} 
	
	Os exerc\'{\i}cios:

	\begin{enumerate}
		\item $rev(\xcat xy) = \xcat{(rev\ y)}{(rev\ x)}$
		\item O operador \xcat xy \'e associativo.
		\item $rev\ rev = id$
		\item $b\in\xsnoc xc = b\in x \lor b = c$
	\end{enumerate}
\end{ex}

\section{Os testes}

\begin{ex}
	Use a metodologia dos exerc\'{\i}cios anteriores para 
	resolver as quest\~oes dos testes $\mathcal{S}_0$ e $\mathcal{S}_1$.

\end{ex}

\begin{ex}
	Use seu provador e formalize as solu\c{c}\~oes dos exerc\'{\i}cios 
	$\mathcal{S}_0$ e $\mathcal{S}_1$. Anote todos os problemas que voc\^e 
	encontrou.
\end{ex}



\end{document}

