117366 - Lógica Computacional 1

Table of Contents

Quadro de avisos:

  • Plano de Ensino
  • Uma longa noite aprendendo
  • Todos os emails enviados ao professor devem conter a expressão [LC1] no assunto da mensagem.
  • Uma cópia da bibliografia principal da disciplina pode ser encontrada na copiadora que fica no final da ala norte do ICC (pasta 22)
  • [2018-08-13 Seg 17:52]: Leitura sobre indução matemática: pdf
  • [2018-08-29 Qua 18:44]: Monitoria de LC1: Todas as segundas e quartas de 18h às 19h, iniciando em [2018-09-03 Seg].
    • Local: PAT AT 021.
  • [2018-08-30 Qui 09:34]: Primeira lista de exercícios (pdf)
    • Gabarito: pdf
  • [2018-09-05 Qua 15:44]: Cancelada a monitoria de hoje!
  • [2018-09-19 Qua 20:35]: Gabarito da prova 1 (pdf)
  • [2018-09-24 Seg 18:06]: A revisão da prova 1 será realizada no dia [2018-10-01 Seg 17:45]–[2018-10-01 Seg 18:15]
  • [2018-09-26 Qua 11:34]: Atividade sobre indução (link)
    • A data limite para a formação dos grupos é [2018-10-11 Qui]
    • Esta atividade pode ser realizada em grupos de até 4 alunos. Ao clicar no link, o aluno pode criar um novo grupo, ou entrar em um grupo já existente. O objetivo desta atividade é fortalecer os conhecimentos sobre indução, e aplicar este conhecimento para resolver um problema computacional interessante.
      • O resultado final desta atividade será um relatório (arquivo pdf) com a solução de dois problemas propostos. Sugiro utilizar Overleaf para gerar o relatório. Veja aqui como integrar o Overleaf com o GitHub.
      • Esta atividade pode ser realizada até o dia [2018-11-18 Dom].
      • Esta tarefa não está prevista no Plano de Ensino, e portanto não é obrigatória. No entanto, dado o baixo resultado na prova 1 (especialmente para os casos indutivos), e considerando que o projeto do curso e a segunda prova têm cobrança ainda maior de questões envolvendo indução, a resolução desta atividade pode ser de grande utilidade.
        • Para os que optarem por fazer esta atividade, a avaliação da mesma será feita de acordo com os seguintes critérios, assumindo um histórico constante de atividades no repositório ao longo dos próximos 50 dias:
          1. Adição de 3.0 pontos na nota da prova 1: relatórios bem escritos e que apresentam soluções completas e corretas para os dois problemas propostos;
          2. Adição de 2.0 pontos na nota da prova 1: relatórios bem escritos, que apresentam uma solução completa e correta para apenas um dos dois problemas propostos, mas que não apresentam erros de utilização dos conceitos apresentados;
          3. Adição de 1.0 ponto na nota da prova 1: relatórios bem escritos, e que apresentam soluções quase completas para os dois problemas propostos, mas não apresentam erros de utilização dos conceitos apresentados;
          4. Os outros casos, incluindo os relatórios com problemas de apresentação, de escrita ou contendo erros na utilização dos conceitos não adicionarão pontuação na nota da prova 1. Este caso inclui repositórios sem histórico de atividades ao longo dos 50 dias de prazo para realização da atividade.
  • [2018-10-17 Qua 18:24]: Projeto PVS (Novo link)
  • [2018-10-22 Seg 10:32]: Palestra "Surprising Mathematics". Prof. Piergiorgio Odifreddi
    • Data: 24 de outubro de 2018
    • Local: Auditório da FT/UnB
    • Divulgação UnB/TV: link
  • [2018-11-05 Seg 15:45]: Segunda lista de exercícios (pdf)

Quadro de Notas:

  Matrícula Grupo Apresentação Relatório Nota Final
1 110027931       0.00
2 150007094       0.00
3 150023502       0.00
4 150080123       0.00
5 150126298       0.00
6 150126760       0.00
7 150140801       0.00
8 150143401       0.00
9 150145527       0.00
10 160005116       0.00
11 160007607       0.00
12 160014522       0.00
13 160027136       0.00
14 160052289       0.00
15 160070431       0.00
16 160117844       0.00
17 160117925       0.00
18 160146682       0.00
19 170012280       0.00
20 170013731       0.00
21 170018997       0.00
22 170023664       0.00
23 170024385       0.00
24 170033813       0.00
25 170038963       0.00
26 170040631       0.00
27 170043665       0.00
28 170057950       0.00
29 170060543       0.00
30 170061001       0.00
31 170069303       0.00
32 170079538       0.00
33 170112624       0.00
34 170144534       0.00
35 170152235       0.00
36 170153304       0.00
37 170153959       0.00
38 170157849       0.00
39 170157962       0.00
40 170163768       0.00
41 180048864       0.00
42 180052667       0.00
          0.00
  Matrícula Prova 1 Prova 2 Projeto Faltas(*) Faltas (%) Nota Final Menção
1 110027931 10.0   0.00 2 6.67 3.00  
2 150007094 2.5   0.00 4 13.33 0.75  
3 150023502 4.5   0.00 3 10.00 1.35  
4 150080123     0.00 18 60.00 0.00 SR
5 150126298 3.0   0.00   0.00 0.90  
6 150126760 10.0   0.00 3 10.00 3.00  
7 150140801 6.5   0.00 2 6.67 1.95  
8 150143401     0.00 8 26.67 0.00 TR
9 150145527     0.00 7 23.33 0.00 TR
10 160005116 5.5   0.00   0.00 1.65  
11 160007607 1.0   0.00 4 13.33 0.30  
12 160014522 5.0   0.00 6 20.00 1.50  
13 160027136 4.0   0.00 3 10.00 1.20  
14 160052289     0.00 2 6.67 0.00 TR
15 160070431 0.0   0.00 1 3.33 0.00  
16 160117844     0.00 21 70.00 0.00 SR
17 160117925 1.5   0.00 2 6.67 0.45  
18 160146682 10.0   0.00 1 3.33 3.00  
19 170012280 4.5   0.00 1 3.33 1.35  
20 170013731 5.5   0.00   0.00 1.65  
21 170018997 8.5   0.00 3 10.00 2.55  
22 170023664 6.0   0.00 1 3.33 1.80  
23 170024385 7.0   0.00   0.00 2.10  
24 170033813 4.5   0.00 1 3.33 1.35  
25 170038963 3.0   0.00 3 10.00 0.90  
26 170040631 5.0   0.00 1 3.33 1.50  
27 170043665 6.0   0.00 1 3.33 1.80  
28 170057950     0.00 4 13.33 0.00 TR
29 170060543 9.0   0.00 1 3.33 2.70  
30 170061001 6.0   0.00 1 3.33 1.80  
31 170069303 0.5   0.00 6 20.00 0.15 TR
32 170079538 1.0   0.00   0.00 0.30  
33 170112624 0.5   0.00 5 16.67 0.15 TR
34 170144534 7.0   0.00 2 6.67 2.10  
35 170152235 0.0   0.00 5 16.67 0.00  
36 170153304     0.00   0.00 0.00 TR
37 170153959 1.0   0.00 5 16.67 0.30 TR
38 170157849 1.0   0.00 5 16.67 0.30 TR
39 170157962 1.0   0.00 5 16.67 0.30 TR
40 170163768 0.0   0.00 5 16.67 0.00  
41 180048864 9.5   0.00   0.00 2.85  
42 180052667 4.5   0.00 1 3.33 1.35  

(*) Última atualização: [2018-11-07 Qua 15:48]

Calendário de aulas:

  1. [2018-08-13 Seg] Introdução e Motivação
    1. Leitura sugerida sobre indução matemática: pdf
    2. Instale o PVS (versão 6.0) no seu computador pessoal
  2. [2018-08-15 Qua] Indução estrutural
    1. Aula no LINF 1
    2. Capítulo 1 (seções 1.1, 1.2 e 1.3), AM17
    3. Exercícios: Considere a estrutura de listas definida como a seguir: \[l ::= [] \mid a::l\]

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

      \[|l| = \left\{\begin{array}{ll} 0, & \mbox{ se } l = [] \\ 1 + |l'|, & \mbox{ se } l = a::l' \end{array}\right.\]

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

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

      1. Prove que \(|l_1 \circ l_2| = |l_1| + |l_2|\), quaisquer que sejam as listas \(l_1, l_2\).
      2. Prove que \(l \circ [] = l\), qualquer que seja a lista l.
      3. Prove que a concatenação de listas é associativa, isto é, \((l_1 \circ l_2)\circ l_3) = l_1 \circ (l_2 \circ l_3)\) quaisquer que sejam as listas \(l_1, l_2\) e \(l_3\).
      4. Prove que \(|rev(l)| = |l|\), qualquer que seja a lista l.
      5. Prove que \(rev(l_1 \circ l_2) = (rev(l_2))\circ (rev(l_1))\), quaisquer que sejam as listas \(l_1, l_2\).
      6. Prove que \(rev(rev(l)) = l\), qualquer que seja a lista l.
    4. Arquivos PVS: exercicio1.pvs exercicio2.pvs
  3. [2018-08-20 Seg] Lógica Proposicional Intuicionista (LPI)
    1. Capítulo 1 (seção 1.4), AM17
      1. Exercícios: 4, 5, 7, 8, 12, 13, 14
  4. [2018-08-22 Qua] Lógica Proposicional Clássica (LPC)
    1. Aula no Pavilhão (PJC BT 101)
    2. Capítulo 1 (seção 1.4), AM17
      1. Exercícios: 6, 9, 10, 11, 15, 16, 17, 18
  5. [2018-08-27 Seg] Exercícios em Dedução Natural (DN)
  6. [2018-08-29 Qua] Semântica da LPC
    1. Aula no LINF 1
    2. Primeira lista de exercícios (pdf)
  7. [2018-09-03 Seg] Correção da LPC
    1. Capítulo 1 (seção 1.6.1), AM17
  8. [2018-09-05 Qua] Completude da LPC
    1. Aula no Pavilhão (PJC BT 101)
    2. Cancelada a monitoria de hoje!
    3. Capítulo 1 (seção 1.6.2), AM17
    4. Sugestão: Fazer todos os exercícios do Capítulo 1, e da lista 1.
  9. [2018-09-10 Seg] Completude da LPC
    1. Lema 3 da seção 1.6.2, AM17
  10. [2018-09-12 Qua] Exercícios de derivação
    1. Gabarito da lista 1: pdf
  11. [2018-09-17 Seg] Exercícios de derivação
  12. [2018-09-19 Qua] Prova 1

    1. Gabarito (pdf)
    2. Atividade sobre indução (link)

    [2018-09-24 Seg] Semana Universitária

    [2018-09-26 Qua] Semana Universitária

  13. [2018-10-01 Seg] Lógica de Predicados (LP) em DN
  14. [2018-10-03 Qua] Correção da LP
  15. [2018-10-08 Seg] Exercícios em DN e o cálculo de sequentes (CS) (caso proposicional)
  16. [2018-10-10 Qua] LP em CS
    1. Aula no LINF 1
  17. [2018-10-15 Seg] Exercícios em CS e CS versus DN
  18. [2018-10-17 Qua] Exercícios em DN e CS, e projeto
    1. Aula no LINF 1
  19. [2018-10-22 Seg] Exercícios em DN e CS, e CS versus DN
  20. [2018-10-24 Qua] Palestra: Surprising Mathematics (Prof. Piergiorgio Odifreddi)
    1. Auditório da FT/UnB
  21. [2018-10-29 Seg] CS versus DN
  22. [2018-10-31 Qua] Projeto
    1. Aula no LINF 1
  23. [2018-11-05 Seg] Completude da LP
  24. [2018-11-07 Qua] Projeto
    1. Aula no LINF 1
  25. [2018-11-12 Seg] Apresentação do Projeto
    1. Local: PJC BT 101
    2. Ordem das apresentações:
      1. Grupo 04
      2. Grup0
      3. lc1
      4. Grupo 01
    3. Apenas os grupos listados acima devem comparecer à apresentação neste dia.
  26. [2018-11-14 Qua] Apresentação do Projeto
    1. Local: PJC BT 101
    2. Ordem das apresentações:
      1. Grupo9
      2. Grupo 007
      3. Grupo 05
      4. Grupo 10
      5. Grupo 02
    3. Apenas os grupos listados acima devem comparecer à apresentação neste dia.
  27. [2018-11-19 Seg] Indecidibilidade da LP
  28. [2018-11-21 Qua] Indecidibilidade da LP
  29. [2018-11-26 Seg] Exercícios em DN e CS
  30. [2018-11-28 Qua] Prova 2

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

Email: contato@flaviomoura.mat.br

Created: 2018-11-10 Sáb 18:49

Validate