\documentclass[12pt]{amsart}
\usepackage{amsmath}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{enumerate}


\input{defport}
\input{deflogic}
\def\stdin{\emph{stdin}}
\def\stdout{\emph{stdout}}
\title{Trabalho 0: \\ Um provador baseado em resolu\cao\\
       Draft 0}

\author{Raul H.C. Lopes}

\begin{document}

\maketitle
\section{Introdu\cao}
O objetivo fundamental deste trabalho consiste em exercitar a constru\cao\
de programas que operam sobre classes indutivas. Para tal você construirá
uma série de programas que operam sobre estruturas de dados clássicas,
cuja natureza indutiva está muito clara: você implementará um provador de
teoremas para lógica de primeira ordem. Neste trabalho, seu provador estará
restrito ao cálculo de proposi\coes\ da lógica clássica. Em outro
trabalho, isso será ampliado para atingir toda a lógica de primeira
ordem. 

Você deverá implementar um módulo (ou conjunto de módulo, dependendo de como
você projetar sua solu\cao), contendo os tipos que definem sua lógica,
tradutores da linguagem externa para os tipos internos do seu provador,
as regras de inferência. Para efeitos deste documento, tudo isso será
aqui identificado como seu \textbf{provador} ou seu \textbf{sistema}
\section{Seu provador e o mundo}
Seu provador entenderá teorias apresentadas usando o cálculo de proposi\coes\
e provar teoremas por contradi\cao. Uma teoria será sempre uma conjun\cao\
de disjun\coes\ de literais. Um literal representará uma verdade atômica
(via variável proposicional) ou a nega\cao\ de uma verdade atômica.
Por exemplo:

\begin{align*}
  p & \text{ verdade atômica, afirmando } p\\
  -p & \text{ a nega\cao\ de } p\\
  p | q & \text{ a afirma\cao\ de que }p\text{ ou }q\text{ valem}\\
  p | -q & \text{ a afirma\cao\ de que }p\text{ ou a nega\cao\ de }q\text{valem}
\end{align*}

Observe o uso de:
\begin{itemize}
  \item $|$ para representar a disjun\cao;
  \item $-$ para representar a nega\cao;
  \item $\&$ para representar a conjun\cao.
\end{itemize}

Seu provador seguirá essas conven\coes. Ele entederá uma teoria como
um conjunto de axiomas e interpretará a mesma como a conjun\cao\ dos axiomas
que a compõem: ou seja, a conjun\cao\ dos axiomas da teoria estará implícita.
Cada axioma será uma disjun\cao\ de literais.

\textbf{Observa\cao\ (e dica):} uma teoria pode ser representada internamente 
como uma \sqn\ de axiomas e um axioma, como uma \sqn\ de literais.

\subsection{A linguagem do seu provador}

A linguagem do seu provador está exposta acima:
\begin{itemize}
  \item teorias serão conjun\coes\ de axiomas, que são, por sua vez, 
disjun\coes\ de literais;
  \item um teorema a provar é qualquer fórmula do cálculo de proposi\coes,
envolvendo conjun\coes e disjun\coes\ de literais.
\end{itemize}

\subsection{Input/output do seu provador}
Seu provador aceitará na linha de comando um string definindo o teorema
a provar e lerá do \stdin\ uma \sqn\ de contendo exatamente um axioma da
teoria por linha.

Ele produzirá como output:
\begin{itemize}
  \ibf{teorema}: Se conseguir provar o teorema em questão.
  \ibf{falha}: Se não conseguir provar o teorema.
\end{itemize}

\subsection{A lógica do seu provador}
Seu provador construirá provas por contradi\cao. Lida a teoria $\Gamma$
e o teorema a provar $\alpha$ ele tentará obter uma contradi\cao\ 
da conjun\cao\ de $\Gamma$ com a nega\cao\ de $\alpha$. Provar:
  \[ \Gamma \& -\alpha \follows \perp\]

Ele deverá realizar a seguinte \sqn\ de passos:
\begin{enumerate}[1.]
  \item Ler teoria;
  \item converter teoria para representa\cao\ interna;
  \item ler teorema a provar;
  \item converter teorema para representa\cao\ interna;
  \item negar teorema (já na sua representa\cao\ interna);
  \item tentar derivar a contradi\cao.
\end{enumerate}

Na tentativa de derivar a contradi\cao\ seu provador usará as seguintes regras.
\begin{itemize}
  \ibf{resolu\cao\ binaria}

Dadas as formulas 
\begin{align*}
   p | C_0 & \text{ e} \\
   -p | C_1 & \text{ derive } \\
   C_0 | C_1 
\end{align*}


\ibf{fatora\cao}

Dada a fórmula 
\begin{align*}
   C_0 | p | C_1 | p | C_2 & \text{ derive} \\
   C_0 | C_1 | C_2 
\end{align*}

\end{itemize}

Uma fórmula vazia (sem literais) representa a contradi\cao. Ela é derivada,
por exemplo, de $p$ e $-p$ por \textbf{resolu\cao} binária.

\section{A execu\cao\ trabalho}

\subsection{As etapas de constru\cao}
Decomponha seu trabalho de acordo com as etapas abaixo.

\subsubsection{Os tipos de dados}
Defina as classes indutivas e os tipos de dados que as representarão
na linguagem de implementa\cao.

\subsubsection{Lendo um axioma}
Defina e implemente e procedimento para converter um string representando um 
axioma (ou uma conjectura) para a representa\cao\ interna do seu sistema.

\subsubsection{Lendo uma teoria}
Defina e implemente procedimento para converter um conjunto de strings 
representando uma teoria para 
a representa\cao\ interna da mesma no seu sistema.

\subsubsection{Negando uma conjectura}
Implementa procedimento que transforma a nega\cao\ de uma conjectura em uma
conjun\cao\ de disjun\coes.

\subsubsection{Apresentando output}
Defina e implemente procedimentos que permitam converter qualquer 
representa\cao\ interna de fórmula para um string em acordo com
a linguagem externa do provador.

\subsubsection{As regras de inferência}
Defina e implementas as regras de inferência acima.

\subsubsection{Estratégias}
Defina e implemente estratégias para melhorar o desempenho do seu provador.

\subsection{Linguagem de programa\cao}
Implemente em Haskell ou C. Se você, adicionalmente, implementar em Isabelle
e provar propriedade de corre\cao\ da sua implementa\cao\ você receberá
mais créditos.
 
\subsection{O que entregar}
Você deverá entregar \emph{tarball} contendo:
\begin{itemize}
  \item A implementa\cao\ do provador;
  \item Módulo de testes;
  \item Documenta\cao\ em \LaTeX;
  \item Makefile 
\end{itemize}

Estando no dirt\'orio de trabalho, compacte seus arquivos com o comando:

\begin{verbatim}
  tar -zhcf tp0.tar.gz *
\end{verbatim}

Teste seu \emph{tarball}, executando  a seguinte \sqn\ de comandos em
um diret\'orio tempor\'ario \textbf{vazio}:
\begin{verbatim}
  tar -zxf tp0.tar.gz
  make all
  make test
\end{verbatim}

Essa \sqn
\subsection{Makefile}

Seu \emph{Makefile} conter\'a dois \emph{targets}:
\begin{itemize}
  \ibf{all}: que ativar\'a a compila\cao\ de todos os programas bem como
a gera\cao\ de documenta\cao\ em \textbf{PDF} a partir dos fontes em \LaTeX.
  \ibf{test}: que ativar\'a o m\'odulo de testes.
\end{itemize}

\subsection{Como entregar}

Submeta seu trabalho por e-mail para

\begin{verbatim}

         raulh@inf.ufes.br

\end{verbatim}

O subject ser\'a:

\centerline{\bf ed:0}

A mensagem conter\'a attachment com o arquivo do trabalho.



\subsection{O m\'odulo de testes}
O m\'odulo de testes consistir\'a neste trabalho simplesmente de um
conjunto de aquivos contendo os axiomas de teoremas e n\~ao teoremas
usados para testar seu provador. Al\'em disso, seu \emph{Makefile}
conter\'a um \emph{target} \textbf{test} que acionar\'a a prova de
cada um teoremas e n\~ao teoremas que constituem o teste. 



\subsection{A avalia\cao}
A nota será atribuída de acordo com a  tabela \ref{pontos}. Note que
um item com pontua\cao\ $* 0.8$ indica que a nota final do trabalho
será multiplicada por $0.8$.

\begin{table}
\begin{tabular}{|l|l|}\hline
  Provador & até $ 8.0$\\
  Módulo de testes & até $1.0$\\
  Documenta\cao & até $1.0$ \\
  Trabalho individual & $* 1.2$ \\
  Trabalho em grupo de 2 & $* 1.0$ \\
  Trabalho em grupo de 3 & $* 0.8$ \\
  Trabalho em grupos de 4 ou mais & $ * 0$\\\hline 
\end{tabular}
\vspace*{0.1cm}
\caption{Pontua\cao\ do trabalho}\label{pontos}
\end{table}



Plágios anulam o trabalho atual e são remetidos imediatamente para 
dire\cao\ do CT, que define puni\cao\ que pode resultar em expulsão 
da universidade.
  
\bibliography{abbrev,analysis,formal,algorithms,program}

\bibliographystyle{amsplain}


\end{document}

