\documentclass[12pt,a4paper]{article}

\usepackage[brazil]{babel}
\usepackage[latin1]{inputenc}

\usepackage{fullpage}

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

\newcounter{conta}
\begin{document}

\noindent P\'os-Gradua\c{c}\~ao em Ci\^{e}ncia da Computa\c{c}\~{a}o
 \hfill DCC/ICEx/UFMG \\
{\it Lógica Aplicada a Computação}
 \hfill $\mbox{2}^{\mbox{\underline{o}}}$ semestre de 2011 \\
Professor: Newton Jos\'{e} Vieira \hfill  nvieira@dcc.ufmg.br \\

\noindent {\bf Plano de Curso}

\section{Pr\'e-requisitos}

Para cursar esta disciplina o aluno dever\'a ter o conhecimento
correspondente \`aquele ministrado nas disciplinas Matem\'atica Discreta (DCC111), Fundamentos da Teoria da Computação
(DCC129) e Algoritmos e Estruturas de Dados II (DCC004).

\section{Programa}

Ser\~ao abordados os seguintes t\'opicos:
\begin{list}{\arabic{conta}}{\usecounter{conta}}
 \item As no\c{c}\~oes de modelagem e formaliza\c{c}\~ao.

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

 \item O problema SAT. Resolu\c{c}\~ao de problemas por codifica\c{c}\~ao
       em l\'ogica proposicional.

 \item Sistemas dedutivos para l\'ogica proposicional.

 \item Raciocínio automatizado em lógica proposicional.

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

 \item Sistemas dedutivos automatizados para l\'ogica de predicados.

 \item Raciocínio automatizado em lógica de predicados.

 \item Infer\^encia em l\'ogica \textit{many-sorted}.

 \item Aplicações: resolução de problemas variados usando solucionadores SAT;
       programação em lógica; demonstração da correção de programas; noções de verificação formal.
\end{list}
 
\section{Bibliografia}
 
O programa ser\'a desenvolvido com base em apostila a ser
distribu\'{\i}da e nos livros:
\begin{enumerate}
 \item Ben-Ari, M. {\em Mathematical Logic for Computer Science\/},
       2nd edition, Springer-Verlag, 2001.
 \item Fitting, M. {\em First-Order Logic and Automated Theorem Proving\/},
       2nd ed., Springer, 1996.
 \item Huth, M.R.A., Ryan, M.D. {\em Logic in Computer Science: Modelling
       and reasoning about systems\/}, 2nd ed., Cambridge University Press,
       2004.
\end{enumerate}

A seguinte lista de livros complementa a apostila e os livros citados com
rela\c c\~ao a alguns t\'opicos do programa:
\begin{enumerate}
 \item Brachman, R.J., Levesque, H.J. {\em Knowledge Representation and Reasoning\/},
       Morgan Kaufmann, 2004.
 \item Enderton, H.B. {\em A Mathematical Introduction to Logic\/}, 2nd ed.,
       Academic Press, 2000.
% \item Gopalakrishnan, G.L. {\em Computation Engineering: Applied automata
%       theory and logic\/}, Springer, 2006.
 \item Harrison, J. {\em Practical Logic and Automated Reasoning\/}, Cambridge Unicersity Press,
       2009.
 \item Nerode, A., Shore, R.A. {\em Logic for Applications\/}, 2nd edition,
       Springer-Verlag, 1997.
 \item Robinson, A., Voronkov, A. (eds.) {\em Handbook of Automated Reasoning\/},
       vols I and II,The MIT Press, 2001.
 \item Russell, S., Norvig, P. {\em Artificial Intelligence: A modern approach\/},
       2nd edition, Prentice Hall, 2003.
% \item Silva, F.S.C., Finger, M., Melo, A.C.V. {\em L\'ogica para
%       Computa\c c\~ao\/}, Pioneira Thomson, 2006.
 \item Smullyan, R.M. {\em First-Order Logic\/}, Dover, 1968.
 \item Smullyan, R.M. {\em Logical Labyrinths\/}, A K Peters Ltd, 2009.
 \item Socher-Ambrosius, R., Johann, P. {\em Deduction Systems\/},
       Springer-Verlag, 1997.
 \item Sterling, L., Shapiro, E. {\em The Art of PROLOG\/}, 2nd ed.,
       MIT Press, 1994.
 \item Tarski, A. {\em Introduction to Logic and to the Methodology of Deductive Sciences\/},
       Dover, 1995.
% \item Veroff, R. (ed.) {\em Automated Reasoning and Its Applications: Essays in
%       honor of Larry Woos\/}, The MIT Press, 1997.
% \item Wos, L., Pieper, G.W. {\em A Fascinating Country in the World of Computing:
%       Your guide to automated reasoning\/}, World Scientific, 1999.
\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\%, 40\% e 30\%, respectivamente.

\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. As no\c{c}\~oes de modelagem e formaliza\c{c}\~ao. \\
 03-04 & 31/10 & \\
 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
 
