\chead{
      \textbf{
          \begin{Large}
          Universidade Federal de Goi\'as\\
          \end{Large}
      \begin{large}INSTITUTO DE MATEM\'ATICA E ESTATISTICA\end{large}\\
      Campus Samambaia -  74001-970 - Goi\^ania\\
      http://www.ime.ufg.br - (62) 3521 1742 - (62) 3521-1208 - secretaria.ime@ufg.br
      }
}


\begin{center}
  \LARGE{\textbf{Plano de Ensino}}
\end{center}

\PlanSection{01. Dados de Identifica\c{c}\~ao da Disciplina:}
{   
   \begin{center}\begin{small}
      \begin{tabular}{|l|p{5cm}|l|p{5cm}|}
         \hline
         \textbf{Semestre:} & 2026.1 &
         \textbf{Curso:} & Matem\'atica Aplicada E Computacional
         \\
         
         \hline
         \textbf{Turma:} & B
         &
         \textbf{C\'odigo Componente:} & IME0463
         \\
         
         \hline
         \textbf{Componente:} & \uppercase{T\'opicos Em Matem\'atica}
         &
         \textbf{UA Respons\'avel:} & IME
         \\
         
         \hline
         \textbf{Carga Hor\'aria:} & 64
         &
         \textbf{UA Solicitante:} & IME
         \\
         
         \hline
         \textbf{Te\'orica/Pr\'atica:}
         &
         64/-
         &
         
         \textbf{EAD/PCC:}
         &
         -/-
         \\
         
         
         \hline
         \textbf{Hor\'arios:}
         &
         35T56
         &
         
         \textbf{Docente:}
         &
         Prof(a) Thaynara Arielly De Lima
         \\
         
         \hline
      \end{tabular}
   \end{small}\end{center}
}

\PlanSection{02. Ementa:}
{
  Deriva\c{c}\~ao e Provas na L\'ogica Proposicional. Deriva\c{c}\~ao e Provas na L\'ogica de Predicados.
Dedu\c{c}\~oes no estilo de C\'alculo de Sequentes \`a la Gentzen. Deriva\c{c}\~oes e Formaliza\c{c}\~oes no
assistente PVS.
}


\PlanSection{03. Programa:}
{
  \begin{enumerate}
\item[1.] Deriva\c{c}\~ao e Provas na L\'ogica Proposicional: Sintaxe da L\'ogica Proposicional; Indu\c{c}\~ao Estrutural; Dedu\c{c}\~ao 
Natural (DN) e Provas na L\'ogica Proposicional; Sem\^antica da L\'ogica Proposicional; Corre\c{c}\~ao e Completude de DN 
na L\'ogica Proposicional.
\item[2.] Deriva\c{c}\~ao e Provas na L\'ogica de Predicados: Sintaxe da L\'ogica de Predicados; Dedu\c{c}\~ao Natural (DN) e 
Provas na L\'ogica de Predicados; Sem\^antica da L\'ogica de Predicados; Corre\c{c}\~ao e Completude de DN na L\'ogica de 
Predicados. Indecidibilidade da L\'ogica de Predicados.
\item[3.] Dedu\c{c}\~oes no estilo de C\'alculo de Sequentes \`a la Gentzen: C\'alculo de Sequentes \`a la Gentzen na L\'ogica de 
Predicados; C\'alculo de Sequentes \`a la Gentzen Intuicionista. Dedu\c{c}\~ao Natural vs Dedu\c{c}\~ao \`a la Gentzen.
\item[4.] Deriva\c{c}\~oes e Formaliza\c{c}\~oes no assistente PVS: O sistema Prototype Verification System (PVS). 
Formaliza\c{c}\~oes em PVS vs. Deriva\c{c}\~oes. Comandos em PVS para manipula\c{c}\~oes equacionais. Comandos em PVS para 
Indu\c{c}\~ao. Exemplos de Formaliza\c{c}\~oes em PVS.
\end{enumerate}
}


\PlanSection{04. Cronograma:}
{
  \\begin{enumerate}
 \item \textbf{Deriva\c{c}\~ao e Provas na L\'ogica Proposicional:} 14 horas-aula.
 \item \textbf{Deriva\c{c}\~ao e Provas na L\'ogica de Predicados:} 14 horas-aula.
 \item \textbf{Dedu\c{c}\~oes no estilo de C\'alculo de Sequentes \`a la Gentzen:} 14 horas-aula.
 \item \textbf{Deriva\c{c}\~oes e Formaliza\c{c}\~oes no assistente PVS:} 14 horas-aula.
 \item \textbf{Atividade Avaliativas:} 8 horas-aula.
\end{enumerate}
}


\PlanSection{05. Objetivos Gerais:}
{
  Estudar diferentes sistemas de dedu\c{c}\~ao em L\'ogica Proposicional e de Predicados e aplica\c{c}\~oes.
}



\PlanSection{06. Objetivos Espec\'{\i}ficos:}
{
  Estudar os sistemas de dedu\c{c}\~ao natural (DN) intuicionista e cl\'assico nas L\'ogicas Proposicional e de Predicados. 
Estabelecer a corre\c{c}\~ao e completude de DN cl\'assico. Entender o sistema de dedu\c{c}\~ao \`a la Gentzen e sua 
correla\c{c}\~ao com DN. Conhecer o assistente de prova \textit{Prototype Verification System (PVS)} e a correla\c{c}\~ao de 
seus comandos com regras do sistema \`a la Gentzen.
Desenvolver formaliza\c{c}\~oes em PVS.
}


\PlanSection{07. Metodologia:}
{
  O programa ser\'a 
desenvolvido de modo expositivo,
baseado na
resolu\c{c}\~ao de 
exerc\'{\i}cios, 
discuss\~oes de 
problemas, 
demonstra\c{c}\~oes de resultados e 
utiliza\c{c}\~ao de recursos 
digitais, al\'em da 
explora\c{c}\~ao de
ferramentas com 
abordagens 
computacionais 
(Prototype Verification System (PVS), Isabelle/HOL). 
Ser\~ao 
disponibilizadas listas 
de exerc\'{\i}cios, visando 
a cria\c{c}\~ao do h\'abito 
de estudo frequente e 
a an\'alise dos 
conte\'udos 
abordados, al\'em de 
promover o 
desenvolvimento de 
habilidades e 
incentivar a 
criatividade na 
resolu\c{c}\~ao de 
problemas. Ser\'a 
valorizada a utiliza\c{c}\~ao 
de outras 
bibliografias para 
complementa\c{c}\~ao 
te\'orica e pr\'atica, e 
exemplos adicionais. 
Tamb\'em ser\'a 
proposto o 
desenvolvimento de 
um projeto, a fim de 
oportunizar aos 
discentes aplica\c{c}\~oes 
pr\'aticas dos m\'etodos 
abordados e 
realiza\c{c}\~ao de 
atividades de 
investiga\c{c}\~ao.
Durante a disciplina, o pesquisador Mariano Moscato (AMA/NASA LaRC) ir\'a, com colabora\c{c}\~ao da professora da 
disciplina, ofertar um curso de PVS para os alunos, com dura\c{c}\~ao de duas aulas (28 e 30 de abril). Com esta a\c{c}\~ao, 
pretende-se fomentar a intera\c{c}\~ao 
dos discentes com pesquisadores na \'area, oportunizando o interc\^ambio de ideias e o contato com expertos, al\'em 
dos professores da Universidade. 

A
professora far\'a, 
quando necess\'ario, 
altera\c{c}\~ao na ordem 
das unidades do 
conte\'udo 
program\'atico e a 
redistribui\c{c}\~ao das 
horas destinadas a 
cada t\'opico.
\\

{\bf Observa\c{c}\~ao:} As 
atividades 
supervisionadas 
mencionadas no Art. 
16 do RGCG ser\~ao 
apresentadas pelo 
professor em sala de 
aula e 
supervisionadas no 
hor\'ario de 
atendimento da 
disciplina.
}


\PlanSection{08. Avalia\c{c}\~oes:}
{
  A avalia\c{c}\~ao ser\'a composta de dois instrumentos: uma prova 
escrita individual e o desenvolvimento de um projeto em 
equipe que visa a formaliza\c{c}\~ao em PVS de um problema, a ser designado pela professora. As datas previstas para 
a 
realiza\c{c}\~ao das avalia\c{c}\~oes (prova e projeto) s\~ao:\\
Prova : 21/05/2026\\
Projeto: \\
(i) Data final para defini\c{c}\~ao de equipes: 19/05/2026. \\
(ii) Entrega do documento escrito: 18/06/2026. \\
(iii) Apresenta\c{c}\~oes: Aulas de 18/06/2026, 23/06/2026 e 25/06/2026.

A m\'edia final (MF) ser\'a dada pela m\'edia aritm\'etica das duas 
notas: prova e projeto. 
\\

\indent{\bf Observa\c{c}\~oes:} \\
\indent 1 - Avalia\c{c}\~oes de segunda chamada somente ser\~ao 
aplicadas segundo as normas previstas na Resolu\c{c}\~ao 
correspondente, dentro do prazo estabelecido pela Resolu\c{c}\~ao, 
com as devidas justificativas. \\
\indent 2 - N\~ao haver\'a avalia\c{c}\~ao substitutiva.\\
\indent 3 - As notas das avalia\c{c}\~oes ser\~ao divulgadas em sala de 
aula e no SIGAA. \\
\indent 4- As avalia\c{c}\~oes de segunda chamada dos pedidos 
deferidos ocorrer\~ao ao final do curso, especificamente no dia
30/06/2026.
}


\PlanSection{09. Bibliografia:}
{
  \textbf{[1]:} AYALA-RINC\'ON, M. ; DE MOURA, F. L. C. Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs. Springer, 2017.

\textbf{[2]:} SOUZA, J. N. L\'ogica para Ci\^encia da Computa\c{c}\~ao. 3. ed. Editora Campus, 2015.

\textbf{[3]:} HUTH, Michael; RYAN, Mark. L\'ogica em Ci\^encia da Computa\c{c}\~ao: modelagem e argumenta\c{c}\~ao sobre sistemas. 2. ed. Editora LTC, 2008.


}

\PlanSection{10. Bibliografia Complementar:}
{
  \textbf{[1]:} HARRISON, J. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.

\textbf{[2]:} CHANG, C.L; LEE, R. C.T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

\textbf{[3]:} ENDERTON, H. A. Mathematical Introduction to Logic. Academic Press, 2000.

\textbf{[4]:} HODEL, R. E. An Introduction to Mathematical Logic. Dover, 1995.

\textbf{[5]:} TROELSTRA, A. S.; SCHWICHTENBERG, H. Basic Proof Theory. Cambridge University Press, 2000.


}

\PlanSection{11.  Livros Texto:}
{
   
}


\PlanSection{12. Hor\'arios:}
{
   \begin{center}
\begin{small}
\begin{tabular}{lll}
\hline
   \textbf{Dia} & \textbf{Hor\'ario} & \textbf{Sala Distribuida}\\
\hline

   3$^a$ & T5 & 208, CAA (50)\\
   3$^a$ & T6 & 208, CAA (50)\\
   5$^a$ & T5 & 105, CAA (50)\\
   5$^a$ & T6 & 105, CAA (50)\\
\end{tabular}
\end{small}\end{center}

}


\PlanSection{13. Hor\'ario de Atendimento do(a)s Professor(a):}
{
   \begin{small}
\begin{tabular}{ll}
   \textbf{1. } & Ter\c{c}as, 15:45 - 16:15, Sala dos professores CA Baru\\
   \textbf{2. } & Quintas, 16:00 - 16:30, Sala dos professores CA Aroeira\\
\end{tabular}
\end{small}
}

\PlanSection{14. Professor(a):}
{
   \begin{small}
\begin{tabular}{lll}
   Thaynara Arielly De Lima. & Email: thaynaradelima@ufg.br, & IME\\
\end{tabular}
\end{small}
}




\vspace{0.2cm}

\begin{center}
\underline{\hspace{8cm}}\\\small{Prof(a) Thaynara Arielly De Lima}\end{center}