\documentclass[12pt,a4paper]{article}

\usepackage[portuguese]{babel}

\usepackage{fullpage}

%=================================================================
\addtolength{\topmargin}{.5cm}
%\addtolength{\textheight}{3cm}
%\addtolength{\evensidemargin}{-2cm}
%\addtolength{\textwidth}{2.5cm}
%=================================================================

\newcounter{conta}
\begin{document}
 
\noindent Universidade Federal de Minas Gerais
 
\noindent {\it L\'ogica Aplicada a Computa\c{c}\~ao}
\hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2003 \\ 
\noindent Professor: Newton Jos\'{e} Vieira \hfill e-mail: nvieira@dcc.ufmg.br \\
\noindent {\bf Plano de Curso}

\section{Pr\'e-requisitos}

Para cursar esta disciplina o aluno j\'a dever\'a ter cursado Matem\'atica
Discreta e Algoritmos e Estruturas de Dados III.

\section{Programa}
 
\begin{list}{\arabic{conta}}{\usecounter{conta}}
 \item L\'ogica proposicional: sintaxe e sem\^antica.

 \item Sistemas dedutivos para l\'ogica proposicinal: de Hilbert,
       de dedu\c c\~ao natural, de tableaux sem\^anticos, de Gentzen,
       de resolu\c c\~ao.

 \item  BDDs ({\em Binary Decision Diagrams\/}).

 \item L\'ogica de predicados: sintaxe e sem\^antica.

 \item Sistemas dedutivos para l\'ogica de predicados: de Hilbert,
       de dedu\c c\~ao natural, de tableaux sem\^anticos, de Gentzen,
       de resolu\c c\~ao.

 \item Programa\c c\~ao em l\'ogica: {\em SLD-resolution\/}, Prolog.

 \item Programas: sem\^antica e verifica\c c\~ao.

 \item Programas: especifica\c c\~ao formal em Z.

 \item L\'ogica temporal: sintaxe e sem\^antica, tableaux.

 \item Verifica\c c\~ao por {\em model checking\/}.
\end{list}
 
\section{Bibliografia}
 
O programa ser\'a desenvolvido em sua maioria com base no livro:
\begin{enumerate}
 \item[\ ] Ben-Ari, M. {\em Mathematical Logic for Computer Science\/},
           2nd edition, Springer-Verlag, 2001.
\end{enumerate}

A seguinte lista de livros complementa o livro citado com rela\c c\~ao a
alguns t\'opicos do programa. Alguns cont\^em tamb\'em t\'opicos
que n\~ao ser\~ao cobertos no curso, menos por falta de import\^ancia do
que por limita\c c\~ao de tempo.

\begin{enumerate}
 \item Bratko, I. {\it PROLOG Programming for Artificial Intelligence\/},
       3rd edition, Addison-Wesley, 2001.
 \item Burke, E., Foxley, E. {\em Logic and Its Applications\/}, Prentice
       Hall, 1996.
 \item Huth, M.R.A., Ryan, M.D. {\em Logic in Computer Science: Modelling
       and Reasoning about Systems\/}, Cambridge University Press, 2000.
 \item Moura, A.V. {\em Especifica\c c\~oes em Z: Uma Introdu\c c\~ao\/},
       Editora da UNICAMP, 2001.
 \item Nerode, A., Shore, R.A. {\em Logic for Applications\/}, 2nd edition,
       Springer-Verlag, 1997.
 \item Nissanke, N. {\em Introductory Logic and Sets for Computer
       Scientists\/}, Addison-Wesley, 1999.
 \item Reeves, S., Clarke, M. {\em Logic for Computer Science\/},
       Addison-Wesley, 1990.
 \item Socher-Ambrosius, R., Johann, P. {\em Deduction Systems\/},
       Springer-Verlag, 1997.
 \item Souza, J.N., {\em L\'ogica para Ci\^encia da Computa\c c\~ao\/},
       Campus, 2002.
 \item Sterling, L., Shapiro, E. {\em The Art of PROLOG\/},
       MIT Press, 1986.
 \item Velleman, D.J., {\em How To Prove It: A Structured Approach\/},
       Cambridge University Press, 1994.
\end{enumerate}

\section{Avalia\c{c}\~ao}

A avalia\c c\~ao ser\'a feita por meio de listas de exerc\'{\i}cios, trabalhos
pr\'aticos e provas, na propor\c c\~ao de 30\%, 30\% e 40\%, repectivamente.

\end{document}
\section{Cronograma das Aulas}

\begin{tabular}{rcl}
 \multicolumn{1}{c}{\it Aula} & {\it Data} & \multicolumn{1}{c}{\it Assunto} \\
 01-02 & 29/10 & Apresenta\c{c}\~{a}o do plano de curso \\
 03-04 & 31/10 & 1.1, 1.2, 1.3 \\
 05-06 & 05/11 & 1.4, 1.5, 1.6 \\
 07-08 & 07/11 & 1.7, 1.8, 1.9 \\
 09-10 & 12/11 & 1.10, 1.11, 1.12 \\ 
 11-12 & 14/11 & 2.1 \\
 13-14 & 19/11 & 2.2.1, 2.2.2 \\
 15-16 & 21/11 & 2.2.3 \\
 17-18 & 26/11 & 2.3.1, 2.3.2 \\
 19-20 & 28/11 & Prova (at\'e se\c c\~ao 2.2) \\
 21-22 & 03/12 & 2.3.3, 2.4.1, 2.4.2 \\
 23-24 & 05/12 & 2.5 \\
 25-26 & 10/12 & 2.6 \\
 27-28 & 12/12 & 2.7, 2.8 \\
 29-30 & 17/12 & 3.1, 3.2 \\
 31-32 & 19/12 & Prova (cap\'{\i}tulo 2)\\
 33-34 & 07/01 & 3.3 \\
 35-36 & 09/01 & 3.4.1, 3.4.2 \\
 37-38 & 14/01 & 3.4.3 \\
 39-40 & 16/01 & 3.4.4 \\
 41-42 & 21/01 & 3.5 \\
 43-44 & 23/01 & 4.1 \\
 45-46 & 28/01 & Prova (at\'e cap\'{\i}tulo 3) \\
 47-48 & 30/01 & 4.2 \\
 49-50 & 04/02 & 4.3, 4.4 \\
 51-52 & 06/02 & 5.1 \\
 53-54 & 11/02 & 5.2, 5.3 \\
 55-56 & 13/02 & 5.4, 5.5 \\
 57-58 & 18/02 & Revis\~{a}o \\
 59-60 & 20/02 & Prova (toda a mat\'eria) \\
\end{tabular}
 
\end{document}
\endinput
\end
 
