117366 - Lógica Computacional 1 (Turma D)

Table of Contents

Quadro de avisos:

  • Plano de ensino
  • Todos os emails enviados ao professor devem conter a expressão [LC1] no assunto da mensagem.
  • A bibliografia principal da disciplina pode ser encontrada no site da Springer ou na Amazon. Uma cópia do capítulo 1 para uso na disciplina está disponível na pasta 22 da copiadora localizada no térreo do final do ICC norte.
  • Uma longa noite aprendendo
  • Monitoria (Gabriel Oliveira Taumaturgo - gabrieloliveiraunb@gmail.com)
  • Monitoria extra (com Lucas Ângelo da Silveira lucas.angel9@gmail.com):
    • [2017-04-05 Qua 18:00]–[2017-04-05 Qua 19:00]
      • Local: PJC BT 101
    • [2017-04-10 Seg 18:00]–[2017-04-10 Seg 19:00]
      • Local: PJC BT 101
    • [2017-04-11 Ter 18:00]–[2017-04-11 Ter 19:00]
      • Local: PJC BT 101
  • Listas de exercícios adicionais: link
  • Aulas no LINF 4: A partir de [2017-04-27 Qui] as aulas das quintas-feiras serão realizadas no LINF4. Esta mudança permanecerá até o final do semestre.
  • Uma cópia do capítulo 2 das notas de aula está disponível na *pasta 22 da copiadora localizada no térreo do final do ICC norte.
  • Gabarito da *prova 1 (pdf)
  • Revisão da prova 1: <2017-05-02 Ter 12:00>–<2017-05-02 Ter 13:00>
  • Uma cópia do capítulo 3 das notas de aula está disponível na *pasta 22 da copiadora localizada no térreo do final do ICC norte.
  • Projeto: O trabalho deste semestre consiste em provar a correção do algoritmo de ordenação por inserção em vetores (que serão chamados de sequências em PVS).
    • Enunciado do projeto: pdf
    • Arquivos PVS: tgz
  • Uma cópia dos capítulos 4, 5 e 6 das notas de aula está disponível na *pasta 22 da copiadora localizada no térreo do final do ICC norte.
  • Lista de exercícios: link
  • Monitoria extra (Gabriel Oliveira Taumaturgo - gabrieloliveiraunb@gmail.com)
    • Local: LINF
    • Horário: 12h - 13h30
    • Dia: [2017-06-22 Qui]

Quadro de Notas

Matrícula Grupos [2017-01-03 Ter] [2017-01-05 Qui] Apresentação Relatório Nota Final Arquivos
100123571 7 (OK)     5   3 Email from Silas Souza
110012496 - - -     0 -
110024702 4     0   0  
110028384 4     0   0  
110148746 4     0   0  
120125471 - - -     0 -
120129647 3 (OK)     10   6  
120151898 3 (faltou)     0   0  
130024902 - - -     0 -
140030395 1 (OK)     10   6 Email from Rafael Alves Fernandes
140083162 6 (OK)     10   6 Email from Ismael Medeiros
140135910 3 (OK)     10   6  
140142959 8 (OK)     8   4.8 Email from Hélio Santana
140145621 9     0   0  
140156429 - - -     0 -
140159932 - - -     0 -
150004354 4     0   0  
150009101 2 (OK)     10   6 Email from Emily Souza
150014961 2 (OK)     10   6  
150015585 3 (OK)     10   6 Email from Luan Freitas
150048718 1 (OK)     10   6  
150124236 11     0   0  
150126158       0   0  
150126808 5 (OK)     5   3 Email from Matheus Rodrigues
150141661 5 (faltou)     0   0  
150146612 5 (OK)     5   3  
160008981 10     0   0  
160014522       0   0  
160113121 11     0   0  
160116929 - - -     0 -
160123283       0   0  
160125260 2 (OK)     10   6  
160127815 2 (OK)     10   6  
160141575 - - -     0 -
160146712 - - -     0 -
170037100 - - -     0 -
170080846       0   0  
        0   0  
Matrícula Prova 1 Prova 2 Média das provas Projeto Faltas(*) Faltas (%) Nota Final Menção
100123571 1.5   0.64285714 3 5 15.625 1.35  
110012496     0 0 25 78.125 0 SR
110024702 8.5   3.6428571 0 5 15.625 2.55  
110028384 1.5   0.64285714 0 4 12.5 0.45  
110148746 2.0   0.85714286 0 5 15.625 0.6  
120125471 3.5   1.5 0 16 50 1.05 SR
120129647 0.5   0.21428571 6 1 3.125 1.95  
120151898 1.0   0.42857143 0 6 18.75 0.3  
130024902 0.0   0. 0 4 12.5 0. TR
140030395 10.0   4.2857143 6 1 3.125 4.8  
140083162 3.5   1.5 6 2 6.25 2.85  
140135910 5.5   2.3571429 6 1 3.125 3.45  
140142959 3.5   1.5 4.8 2 6.25 2.49  
140145621 1.0   0.42857143 0 5 15.625 0.3  
140156429     0 0 22 68.75 0 SR
140159932     0 0 15 46.875 0 SR
150004354 2.0   0.85714286 0 7 21.875 0.6  
150009101 7.5   3.2142857 6 2 6.25 4.05  
150014961 7.5   3.2142857 6 1 3.125 4.05  
150015585 5.0   2.1428571 6 2 6.25 3.3  
150048718 5.0   2.1428571 6 1 3.125 3.3  
150124236 3.5   1.5 0 4 12.5 1.05  
150126158 2.0   0.85714286 0 13 40.625 0.6 SR
150126808 9.0   3.8571429 3 1 3.125 3.6  
150141661 8.0   3.4285714 0 0 0 2.4  
150146612 7.0   3. 3 2 6.25 3.  
160008981     0 0 8 25 0  
160014522 2.5   1.0714286 0 7 21.875 0.75  
160113121 6.5   2.7857143 0 3 9.375 1.95  
160116929     0 0 5 15.625 0 TR
160123283 1.0   0.42857143 0 6 18.75 0.3  
160125260 0.5   0.21428571 6 3 9.375 1.95  
160127815 4.5   1.9285714 6 3 9.375 3.15  
160141575 2.0   0.85714286 0 2 6.25 0.6 TR
160146712     0 0 9 28.125 0 TR
170037100     0 0 14 43.75 0 TR
170080846 1.5   0.64285714 0 6 18.75 0.45  
Média     0 0   0 0  

(*) Última atualização: [2017-05-29 Seg 15:01]

Calendário de aulas

<2017-03-07 Ter 10:00>–<2017-03-07 Ter 11:50> 1. Introdução e motivação ✓

<2017-03-09 Qui 10:00>–<2017-03-09 Qui 11:50> 2. Lógica Proposicional Intuicionista ✓

  • Dedução Natural

<2017-03-14 Ter 10:00>–<2017-03-14 Ter 11:50> 3. Indução matemática ✓

  • [2017-03-14 Ter 16:18]: Leitura recomendada (com exercícios!): pdf

<2017-03-16 Qui 10:00>–<2017-03-16 Qui 11:50> 4. Exercícios de DN ✓

  • Fazer todos os exercícios apresentados no capítulo 1 das notas de aula.

<2017-03-21 Ter 10:00>–<2017-03-21 Ter 11:50> 5. Indução e provas ✓

  • Exercício: Considere a estrutura de listas definida como a seguir: \[l ::= nil \mid cons(a,l)\]

    onde \(nil\) representa a lista vazia, e \(cons(a,l)\) representa a lista com primeiro elemento \(a\) e cauda \(l\). O comprimento de uma lista é definido recursivamente por:

    \[length(l) = \left\{\begin{array}{ll} 0, & \mbox{ se } l = nil \\ 1 + length(l'), & \mbox{ se } l = cons(a,l') \end{array}\right.\]

    A concatenação de listas também pode ser definida por uma função recursiva: \[concat(l_1,l_2) = \left\{\begin{array}{ll} l_2, & \mbox{ se } l_1 = nil \\ cons(a, concat(l',l_2)), & \mbox{ se } l_1 = cons(a,l') \end{array}\right.\]

    O reverso de listas é definido por: \[rev(l) = \left\{\begin{array}{ll} l, & \mbox{ se } l = nil \\ concat(rev(l'), cons(a,nil)), & \mbox{ se } l = cons(a,l') \end{array}\right.\]

    1. Prove que \(length(concat(l_1, l_2)) = length(l_1) + length(l_2)\), para listas \(l_1, l_2\) quaisquer. (Feito em sala).
    2. Prove que \(concat(l, nil) = l\), para qualquer lista l.
    3. Prove que \(concat(concat(l_1, l_2), l_3) = concat(l_1, concat(l_2, l_3))\) para listas \(l_1, l_2\) e \(l_3\) quaisquer.
    4. Prove que \(length(rev(l)) = length(l)\), para qualquer lista l.
    5. Prove que \(rev(concat(l_1,l_2)) = concat(rev(l_2), rev(l_1))\), para listas \(l_1, l_2\) quaisquer.
    6. Prove que \(rev(rev(l)) = l\), para qualquer lista l.
  • Exercício adicional: Refaça os exercícios acima em PVS. Arquivo com os enunciados dos exercícios: lists.pvs
    • Alguns comandos que podem ser úteis:
      1. (skeep): funciona como a regra (\(\forall_i\)) seguida de eventuais simplificações. Se você precisa provar uma fórmula da forma \(\forall x p(x)\) então o PVS introduz uma nova variável arbitrária \(x\) no contexto, e pede para provarmos \(p(x)\).
      2. (expand "def" fnum (pos1 pos2 ... posn)): aplica a definição def nas posições pos1, pos2, ..., posn da fórmula fnum.
      3. (induct "n"): aplica o princípio da indução matemática na variável n.
      4. (lemma "name"): adiciona o lema de nome "name" nas hipóteses.
      5. (replace fnum gnum): se a fórmula numerada com fnum for da forma \(A = B\), todas as ocorrências de \(A\) na fórmula numerada com gnum são substituídas por \(B\).
      6. (rewrite fnum gnum): se a fórmula numerada com fnum for da forma \(A = B\), todas as ocorrências de instâncias de \(A\) na fórmula numerada com gnum são substituídas por instâncias correspondentes de \(B\).
      7. (assert): realiza as simplificações possíveis.
      8. M-x view-prelude-file: abre o arquivo contendo a biblioteca básica do PVS. Aqui podem ser encontradas diversas definições e provas de propriedades que podem ser úteis no desenvolvimento de novas provas.

<2017-03-23 Qui 10:00>–<2017-03-23 Qui 11:50> 6. Lógica Proposicional Clássica ✓

  • Dedução Natural
  • Exercício: Prove a que a lei de Peirce é uma regra clássica.

<2017-03-28 Ter 10:00>–<2017-03-28 Ter 11:50> 7. Exercícios de DN ✓

<2017-03-30 Qui 10:00>–<2017-03-30 Qui 11:50> 8. Semântica da Lógica Proposicional Clássica ✓

<2017-04-04 Ter 10:00>–<2017-04-04 Ter 11:50> 9. Correção da Lógica Proposicional Clássica ✓

  • Exercícios sugeridos: Completar as provas iniciadas em aula: teorema de Glivenko, equivalência entre um fórmula e sua dupla negação no fragmento negativo da lógica proposicional (exercício 14, seção 1.4) das notas de aula, teorema da correção da lógica proposicional.

<2017-04-06 Qui 10:00>–<2017-04-06 Qui 11:50> 10. Completude da Lógica Proposicional Clássica ✓

  • Listas de exercícios adicionais:
    • [2017-04-06 Qui 12:52] Dedução Natural: pdf ([2017-04-13 Qui 03:49]: gabarito)
    • [2017-04-06 Qui 12:52]: Exercícios de revisão de indução: pdf ([2017-04-13 Qui 03:50]: gabarito)

<2017-04-11 Ter 10:00>–<2017-04-11 Ter 11:50> 11. Completude da Lógica Proposicional Clássica ✓

<2017-04-13 Qui 10:00>–<2017-04-13 Qui 11:50> 12. Aula de exercícios ✓

<2017-04-18 Ter 10:00>–<2017-04-18 Ter 11:50> 13. Prova 1

<2017-04-20 Qui 10:00>–<2017-04-20 Qui 11:50> 14. Lógica de Predicados - Sintaxe ✓

  • Termos, Fórmulas e Substituição

<2017-04-25 Ter 10:00>–<2017-04-25 Ter 11:50> 15. Lógica de Predicados - Dedução Natural ✓

  • Teoria da Prova na Lógica de Predicados
  • Cálculo de sequentes

<2017-04-27 Qui 10:00>–<2017-04-27 Qui 11:50> 16. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4: Prova formal da correção do algoritmo de ordenação por inserção em PVS
    • Arquivo construído hoje em aula: pvs
      • Orientações: Escreva em papel uma prova para o teorema 'iSort_is_correct'. Que resultados auxiliares poderiam ser úteis?

<2017-05-02 Ter 10:00>–<2017-05-02 Ter 11:50> 17. Exercícios de derivação ✓

  • Semântica da Lógica de Predicados
  • Correção do algoritmo de ordenação por inserção

<2017-05-04 Qui 10:00>–<2017-05-04 Qui 11:50> 18. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4: Provar que a função 'insert' preserva ordenação.

<2017-05-09 Ter 10:00>–<2017-05-09 Ter 11:50> 19. CS versus DN (versão intuicionista) ✓

<2017-05-11 Qui 10:00>–<2017-05-11 Qui 11:50> 20. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4.
    • Exercício sugerido: Provar a equivalência entre as duas definições de ordenação

<2017-05-16 Ter 10:00>–<2017-05-16 Ter 11:50> 21. CS versus DN (versão clássica) ✓

<2017-05-18 Qui 10:00>–<2017-05-18 Qui 11:50> 22. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4
    • Exercício sugerido: Completar a prova de equivalência entre as duas definições de ordenação. Uma direção da equivalência foi comentada em aula.

<2017-05-23 Ter 10:00>–<2017-05-23 Ter 11:50> 23. CS versus DN (versão clássica) ✓

<2017-05-25 Qui 10:00>–<2017-05-25 Qui 11:50> 24. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4:

<2017-05-30 Ter 10:00>–<2017-05-30 Ter 11:50> 25. Correção da Lógica de Predicados Clássica e Completude da Lógica de Predicados Clássica ✓

<2017-06-01 Qui 10:00>–<2017-06-01 Qui 11:50> 26. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4:

<2017-06-06 Ter 10:00>–<2017-06-06 Ter 11:50> 27. Completude da Lógica de Predicados Clássica ✓

<2017-06-08 Qui 10:00>–<2017-06-08 Qui 11:50> 28. Aplicações: linguagens de especificação/verificação ✓

  • Aula no LINF 4:

<2017-06-13 Ter 10:00>–<2017-06-13 Ter 11:50> 29. Apresentação do Projeto

<2017-06-15 Qui 08:00>–<2017-06-15 Qui 09:50> Feriado

<2017-06-20 Ter 08:00>–<2017-06-20 Ter 09:50> 30. Exercícios ✓

  • Lista de Exercícios:
    • [2017-06-20 Ter 07:45] Dedução Natural e Cálculo de Sequentes: pdf

<2017-06-22 Qui 08:00>–<2017-06-22 Qui 09:50> 31. Aula de Exercícios

<2017-06-27 Ter 08:00>–<2017-06-27 Ter 09:50> 32. Prova 2

Author: Prof. Flávio L. C. de Moura

Email: contato@flaviomoura.mat.br

Created: 2017-06-20 Ter 13:55

Validate