117366 - Lógica Computacional 1

Table of Contents

Quadro de avisos:

[2019-11-07 Thu 09:43]: A última coluna do quadro de notas está com a ordem das apresentações do projeto, onde (si) denota a i-ésima apresentação da segunda-feira (dia 11), e (qj) denota a j-ésima apresentação da quarta-feira (dia 13). Os projetos serão apresentados no pavilhão (PJC BT 101) a partir dos arquivos disponibilizados no GitHub.

[2019-10-24 Thu 10:33]: A aula do dia [2019-11-04 Mon] será realizada no LINF 5.

[2019-10-16 Wed 16:59]: Segunda lista de exercícios (pdf)

[2019-10-02 Wed 15:13]: Monitoria (Felipe Paradas)

Terças e quintas de 16:00-18:00 na sala de monitoria do CIC/EST.

[2019-10-01 Tue 16:24]: A estagiária de docência Ariane Alves Almeida estará disponível no LaForCE (laboratório 7 do prédio CIC/EST) todas as terças e quintas às 18h para auxílio ao projeto.

[2019-10-01 Tue 16:14]: Enunciado do projeto (pdf) e link para criação dos grupos e acesso aos arquivos pvs. Os grupos podem ser criados até [2019-10-09 Wed 23:00].

[2019-09-28 Sat 11:11]: Não haverá aula no dia [2019-10-02 Wed] (Greve Nacional da Educação)

[2019-09-28 Sat 11:12]: A revisão da prova 1 poderá ser feita no dia [2019-10-07 Mon 15:00]–[2019-10-07 Mon 16:00]

[2019-09-18 Wed 21:42]: Gabarito da prova 1 (pdf)

[2019-09-16 Mon 16:12]: Gabarito da lista de exercícios (pdf)

[2019-09-11 Wed 20:57]: Monitoria: Horários disponíveis antes da primeira prova:

[2019-09-12 Thu 16:00]–[2019-09-12 Thu 18:00] na sala de monitoria CIC/EST.

[2019-09-16 Mon 18:00]–[2019-09-16 Mon 19:00] na sala PAT AT 021.

[2019-09-17 Tue 16:00]–[2019-09-17 Tue 18:00] na sala de monitoria CIC/EST.

[2019-08-29 Thu 10:08]: Primeira lista de exercícios (pdf)

Uma cópia da bibliografia principal AM17 encontra-se disponível na copiadora Exata (pasta 22) localizada no final da ala norte do ICC.

Plano de ensino (pdf)

Cronograma de aulas [79%]

  1. [X] Introdução e Motivação
    • Data: <2019-08-12 Mon 16:00>–<2019-08-12 Mon 17:50>
    • Local: PJC BT 101
    • Resumo da aula:
      • Leitura complementar: pdf
      • Foi apresentada a estrutura geral do curso, incluindo toda a
        informação burocrática. Para a próxima aula, os alunos devem
        ler as seções 1.1, 1.2 e 1.3 da bibliografia principal
        AM17.
  2. [X] Indução estrutural e provas
    • Data: <2019-08-14 Wed 16:00>–<2019-08-14 Wed 17:50>
    • Local: PJC BT 101
    • Resumo da aula: Comentamos as seções 1.1, 1.2 e 1.3 das notas
      de aula a partir das dúvidas apresentadas pelos alunos. Em
      particular, revisitamos a definição de fórmula da lógica
      proposicional e suas diferentes representações. A noção de
      indução também foi explorada em diversos contextos (naturais,
      listas e fórmulas da lógica proposicional). Para a próxima aula,
      os alunos devem ler e trazer dúvidas da seção 1.4 das notas de
      aula: AM17. Para reforçar o estudo das provas por indução,
      sugiro os seguintes exercícios:
      1. Mostre que \(1^2 + 2^2 + ... + n^2 = \frac{n.(n+1).(n+2)}{6}\), ou seja, \(\sum_{i=1}^n i^2 = \frac{n.(n+1).(2.n+1)}{6}\)
      2. Mostre que a soma dos \(n\) primeiros números ímpares é igual a \(n^2\).
      3. Mostre que \(2^n < n! \), para \(n \geq 4\).
      4. Considere a estrutura de listas definida como a seguir: \( l ::= nil \mid a::l \)

        onde \( nil \) 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 = nil \\ 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 = nil \\ 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 = nil \\ (rev(l')) \circ (a :: nil), & \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 nil = 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.
  3. [X] Dedução Natural (DN) na Lógica Proposicional Intuicionista (LPI)
    • Data: <2019-08-19 Mon 16:00>–<2019-08-19 Mon 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.4 de AM17.
    • Leitura complementar: Intuitionistic Logic (Stanford Encyclopedia of Philosophy)
    • Resumo da aula: Um dos exercícios propostos sobre indução foi
      resolvido em detalhes. Em seguida foram apresentadas algumas
      regras do sistema de DN (Tabela 1.2), e foram feitos alguns
      exemplos de derivação: comutatividade da conjunção e da
      disjunção.
  4. [X] DN na Lógica Proposicional Clássica (LPC)
    • Data: <2019-08-21 Wed 16:00>–<2019-08-21 Wed 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.4 de AM17.
    • Resumo da aula: Foram apresentadas caracterizações da LPC. Na
      próxima aula a prioridade será a resolução de exercícios, mas se
      houver tempo, iniciaremos a Seção 1.5 de AM17.
  5. [X] Exercícios em DN
    • Data: <2019-08-26 Mon 16:00>–<2019-08-26 Mon 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.5 de AM17, mas prioritariamente
      resolva todos os exercícios propostos nas notas de aula até a
      Seção 1.4.
    • Resumo da aula: Alguns exercícios foram resolvidos a partir de dúvidas apresentadas pelos alunos:

      • A regra da explosão é uma regra derivada da LPC (exercício 5 de AM17);
      • A dupla negação pode ser propagada sobre a implicação na lógica proposicional minimal, i.e. na LPI sem a regra da explosão;
      • A contrapositiva dada por \(\frac{(\neg \varphi) \to (\neg \psi)}{\psi \to \varphi}\) é tão expressiva quanto a regra de prova por contradição.

      Leitura para a próxima aula: Seções 1.5 e 1.6.1 de AM17.

  6. [X] Semântica da LPC
    • Data: <2019-08-28 Wed 16:00>–<2019-08-28 Wed 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.5 de AM17.
    • Resumo da aula: A aula foi iniciada com uma dúvida relacionada
      ao Teorema de Glivenko (a ser inserido na primeira lista de
      exercícios). Em seguida foram apresentadas as noções de
      consequência lógica, satisfatibilidade e validade, encerrando
      assim, a Seção 1.5. Posteriormente, o PVS foi utilizado para
      resolver as questões propostas sobre listas na aula do dia
      [2019-08-14 Wed]. A solução do primeiro exercício foi iniciada, e
      ficou a cargo dos alunos completar a prova. Arquivo pvs: listas.pvs (listas.prf)
    • Exercício complementar (duplicado para quem está matriculado em
      PAA-B): Considere o Princípio da Indução Matemática (PIM), e o
      Princípio da Indução Forte (PIF) dados a seguir:

      • (PIM) Seja \(P\) uma propriedade sobre os números naturais \(\mathbb{N}\). Se \(P(0)\) (i.e. 0 satisfaz a propriedade \(P\)) e, \(P(k+1)\) assumindo \(P(k)\), para qualquer \(k \geq 0\), então \(P(n)\) para todo \(n \geq 0\). Esquematicamente, temos:

        \begin{equation*} \frac{P(0) \;\;\;\;\;\; \forall k, P(k) \to P(k+1)}{\forall n, P(n)} \end{equation*}
      • (PIF) Seja \(Q\) uma propriedade sobre os números naturais \(\mathbb{N}\). Se pudermos provar \(Q(m)\) assumindo \(Q(k)\) para qualquer \(k < m \), então todo \(n\) satisfaz a propriedade \(Q\):

        \begin{equation*} \frac{\forall m, ( \forall k, k < m \to Q(k) ) \to Q(m)}{\forall n, Q(n)} \end{equation*}

      Mostre que (PIM) e (PIF) são equivalentes, i.e. prove (PIM) utilizando (PIF) como hipótese. Depois assuma (PIM) como hipótese, e prove (PIF).

  7. [X] Correção da LPC
    • Data: <2019-09-02 Mon 16:00>–<2019-09-02 Mon 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.6.1 de AM17.
    • Resumo da aula: A correção da LPC foi provada, mas os detalhes (não apresentados em aula) devem ser estudados a partir das notas de aula. O exercício em PVS iniciado na aula passada foi concluído, e como sugestão, os alunos devem resolver todos os outros exercícios sobre listas propostos na aula do dia [2019-08-14 Wed] no PVS. A partir da próxima aula, em paralelo à teoria, iniciaremos uma formalização da correção do algoritmo de ordenação por inserção em PVS. Arquivo: InsertionSort.pvs
  8. [X] Completude da LPC
    • Data: <2019-09-04 Wed 16:00>–<2019-09-04 Wed 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.6.2 de AM17.
    • Resumo da aula: Foi apresentada a ideia geral da prova do teorema da completude da LPC. Adicionalmente, foi iniciada a formalização da correção (parcial) do algoritmo de ordenação por inserção. Como exercício, os alunos devem provar que a função insert preserva a ordenação. Arquivos: InsertionSort.pvs (InsertionSort.prf)
  9. [X] Completude da LPC
    • Data: <2019-09-09 Mon 16:00>–<2019-09-09 Mon 17:50>
    • Local: PJC BT 101
    • Leitura para a aula: Seção 1.6.2 de AM17.
    • Resumo da aula: Foi apresentada a ideia geral da prova do lema
      principal utilizado na prova do teorema da completude da
      LPC. Algumas dúvidas referentes a exercícios da lista foram
      comentadas.
  10. [X] Exercícios de derivação
    • Data: <2019-09-11 Wed 16:00>–<2019-09-11 Wed 17:50>
    • Local: PJC BT 101
    • Resumo da aula: Resolução de exercícios da lista.
  11. [X] Exercícios de derivação
    • Data: <2019-09-16 Mon 16:00>–<2019-09-16 Mon 17:50>
    • Local: PJC BT 101
    • Resumo da aula: Resolução de exercícios da lista, seguida de
      uma discussão sobre avaliação.
  12. [X] Primeira Prova (Gabarito: pdf)
    • Data: <2019-09-18 Wed 16:00>–<2019-09-18 Wed 17:50>
    • Local: PJC BT 101
    • <2019-09-23 Mon> Semana Universitária
    • <2019-09-25 Wed> Semana Universitária
  13. [X] Lógica de Predicados (LP) em DN
  14. [X] LP em Cálculo de Sequentes (CS)
    • Data: <2019-10-07 Mon 16:00>–<2019-10-07 Mon 17:50>
    • Local: PJC BT 101
    • Resumo da aula: Foram apresentadas as regras estruturais, os
      axiomas, e as regras lógicas envolvendo os conectivos no cálculo
      de sequentes.
  15. [X] Projeto: Radix sort
    • Data: <2019-10-09 Wed 16:00>–<2019-10-09 Wed 17:50>
    • Local: PJC BT 101
    • Resumo da aula: Foram comentados aspectos gerais do projeto, e
      finalizadas as provas da correção parcial do algoritmo
      insertion sort como no arquivos (InsertionSort.pvs e InsertionSort.prf). Para completar a prova de correção é necessário definir a noção de equivalência entre listas, e provar que isort(l) e l são listas equivalentes, qualquer que seja l.
  16. [X] Correção da LP e Aplicações em verificação: linguagens de especificação/verificação
    • Data: <2019-10-14 Mon 16:00>–<2019-10-14 Mon 17:50>
    • Local: LINF 4
  17. [X] Derivação em Assistentes de Prova (AP)
    • Data: <2019-10-16 Wed 16:00>–<2019-10-16 Wed 17:50>
    • Local: LINF 4
  18. [X] Indução, generalização e skolemização em AP
    • Data: <2019-10-21 Mon 16:00>–<2019-10-21 Mon 17:50>
    • Local: LINF 4
  19. [X] Correção de algoritmos
    • Data: <2019-10-23 Wed 16:00>–<2019-10-23 Wed 17:50>
    • Local: LINF 4
  20. [X] DN versus CS
    • Data: <2019-10-28 Mon 16:00>–<2019-10-28 Mon 17:50>
    • Local: LINF 4
  21. [X] DN versus CS
    • Data: <2019-10-30 Wed 16:00>–<2019-10-30 Wed 17:50>
    • Local: LINF 4
  22. [X] DN versus CS
    • Data: <2019-11-04 Mon 16:00>–<2019-11-04 Mon 17:50>
    • Local: LINF 5
  23. [X] Completude da LP
    • Data: <2019-11-06 Wed 16:00>–<2019-11-06 Wed 17:50>
    • Local: LINF 4
  24. [ ] Apresentação do projeto
    • Data: <2019-11-11 Mon 16:00>–<2019-11-11 Mon 17:50>
    • Local: PJC BT 101
  25. [ ] Apresentação do projeto
    • Data: <2019-11-13 Wed 16:00>–<2019-11-13 Wed 17:50>
    • Local: PJC BT 101
  26. [ ] Indecidibilidade da LP
    • Data: <2019-11-18 Mon 16:00>–<2019-11-18 Mon 17:50>
    • Local: PJC BT 101
  27. [ ] Exercícios de derivação
    • Data: <2019-11-20 Wed 16:00>–<2019-11-20 Wed 17:50>
    • Local: PJC BT 101
  28. [ ] Exercícios de derivação
    • Data: <2019-11-25 Mon 16:00>–<2019-11-25 Mon 17:50>
    • Local: PJC BT 101
  29. [ ] Segunda Prova
    • Data: <2019-11-27 Wed 16:00>–<2019-11-27 Wed 17:50>
    • Local: PJC BT 101

Quadro de Notas:

Matrícula Prova 1 Prova 2 Apr Rel Projeto Faltas (*) Faltas(%) Nota Final Menção Obs.
140136282 4.0       0.00 3 10.34 1.20    
140140671         0.00 12 41.38 0.00 SR  
150005491 6.5   7.0   4.20 6 20.69 3.21   (g) (q5)
150052138 4.0   9.0   5.40 4 13.79 2.82   g88 (s6)
150126298 6.5   7.0   4.20 4 13.79 3.21   g10 (q6)
150143401 10.0   7.0   4.20 3 10.34 4.26   g10 (q6)
150147376 7.0   7.0   4.20 2 6.90 3.36   AM (g) (q5)
150153538 6.0   10.0   6.00 1 3.45 3.60   g3 (q2)
160034205 10.0       0.00 6 20.69 3.00    
160046688 0.0       0.00 10 34.48 0.00 TR  
160052289 7.0   7.0   4.20 5 17.24 3.36   g10 (q6)
160071101 9.0       0.00 6 20.69 2.70    
160077907         0.00 5 17.24 0.00 TR  
160115001 5.0   8.0   4.80 6 20.69 2.94   g12 (s5)
160126975 6.0   10.0   6.00 6 20.69 3.60   g8 (q3)
160133670         0.00 16 55.17 0.00 SR  
160135281 10.0   10.0   6.00 1 3.45 4.80   g1 (s2)
160137969 10.0   10.0   6.00 1 3.45 4.80   g8 (q3)
160152658         0.00 4 13.79 0.00 TR  
170010058 6.0   9.0   5.40 5 17.24 3.42   g88 (s6)
170010686         0.00 3 10.34 0.00 TR  
170012387 10.0       0.00 4 13.79 3.00   g2 (s8)
170016641 8.5       0.00 4 13.79 2.55   g2 (s8)
170031870 10.0   10.0   6.00 3 10.34 4.80   g5 (s7)
170043959 8.5   9.0   5.40 3 10.34 4.17   g88 (s6)
170045919 0.0       0.00 10 34.48 0.00 TR  
170050157         0.00 23 79.31 0.00 SR  
170050335 7.0       0.00 3 10.34 2.10    
170058867 10.0   9.0   5.40 1 3.45 4.62   g1 (s2)
170062538 6.0   10.0   6.00 2 6.90 3.60   g5 (s7)
170100863 10.0   7.0   4.20 3 10.34 4.26   g7 (q7)
170103579 10.0       0.00 2 6.90 3.00   g9 (s4)
170105636 6.0   10.0   6.00 1 3.45 3.60   pp (q4)
170112209 6.0   10.0   6.00 1 3.45 3.60   pp (q4)
170113477 10.0   7.0   4.20 3 10.34 4.26   g7 (q7)
170140113 6.0   10.0   6.00 3 10.34 3.60   g8 (q3)
170140997 10.0       0.00 4 13.79 3.00   g9 (s4)
170151140 3.5   10.0   6.00   0.00 2.85   g4 (s1)
170157024 9.0   10.0   6.00 3 10.34 4.50   pp (q4)
180011707 10.0   10.0   6.00 4 13.79 4.80   g11 (s3)
180013696 2.0   8.0   4.80 3 10.34 2.04   g12 (s5)
180019813 0.0       0.00 8 27.59 0.00 TR  
180029479 10.0   10.0   6.00   0.00 4.80   g99 (q1)
180029690 10.0   10.0   6.00 1 3.45 4.80   g3 (q2)
180033808 2.0       0.00 9 31.03 0.60 TR  
180041835 10.0   10.0   6.00 4 13.79 4.80   g99 (q1)
180053906 10.0   10.0   6.00 2 6.90 4.80   g99 (q1)
180074792 10.0   7.0   4.20 2 6.90 4.26   g7 (q7)
180129716         0.00 1 3.45 0.00 TR  
180137531 6.0   7.0   4.20 1 3.45 3.06   (g) (q5)
190012862 6.0   10.0   6.00 3 10.34 3.60   g5 (s7)
Média 7.12       0.00   0.00 2.14    

(*) Última atualização: [2019-11-13 Wed 18:33]

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

Email: contato@flaviomoura.mat.br

Created: 2019-11-13 Wed 18:33

Validate