117366 - Lógica Computacional 1 (Turma B) 2018/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-03-19 Seg 17:56]: Novos exercícios em PVS (pvs)
    • Existe uma tabela de comandos PVS no capítulo 4 das notas de aula (ver item anterior)
  • [2018-03-27 Ter 10:04]: Primeira lista de exercícios pdf (Gabarito: pdf)
  • [2018-04-04 Qua 21:08]: Lista sobre o cálculo de Gentzen pdf (Gabarito: pdf)
  • [2018-04-20 Sex 09:38]: Gabarito da primeira prova: pdf
  • [2018-04-25 Qua 15:07]: Aula de hoje no LINF 2! (Pavilhões fechados)
  • [2018-05-14 Seg 05:38]: Projeto da disciplina
  • [2018-05-20 Dom 22:18]: Revisão da primeira prova: [2018-05-28 Seg 21:00]–[2018-05-28 Seg 21:30]
  • [2018-06-04 Seg 08:44]: Lista de exercícios sobre lógica de predicados (pdf) (gabarito)

Quadro de Notas

Matrícula Grupo Apresentação Relatório Nota Final
110032225 1 9 9 9.00
120116421       0.00
130058866 4     0.00
130110728       0.00
140037454       0.00
140070371 6 8 6.5 7.40
140156089 1 9 9 9.00
140161741 6 8 6.5 7.40
150080123       0.00
150118236 5 9 7 8.20
150120524       0.00
150128576 5 9 7 8.20
150129921 5 9 7 8.20
150136986       0.00
150150610       0.00
160117992 2 9 9 9.00
160120811 2 9 9 9.00
160122295 3     0.00
160122660 2 9 9 9.00
160141168       0.00
160146232 5 9 7 8.20
160148260 2 9 9 9.00
170010481       0.00
170023591 6 8 6.5 7.40
170051579       0.00
170052915       0.00
170065154       0.00
170080846 1 9 9 9.00
170144631 1 9 9 9.00
180046799       0.00
        0.00
Matrícula Prova 1 Prova 2 Projeto Faltas(*) Faltas (%) Nota Final Menção
110032225 5.0   9.00 1 3.12 4.20  
120116421     0.00 3 9.38 0.00 TR
130058866 5.0   0.00 8 25.00 1.50  
130110728 0.0   0.00 5 15.62 0.00  
140037454     0.00 21 65.62 0.00 SR
140070371 2.5   7.40 2 6.25 2.97  
140156089 3.5   9.00 6 18.75 3.75  
140161741 0.0   7.40   0.00 2.22  
150080123 0.0   0.00 11 34.38 0.00 SR
150118236 8.0   8.20 4 12.50 4.86  
150120524     0.00 2 6.25 0.00 TR
150128576 2.5   8.20 2 6.25 3.21  
150129921 8.0   8.20 3 9.38 4.86  
150136986     0.00 14 43.75 0.00 TR
150150610 2.5   0.00 11 34.38 0.75 SR
160117992 0.0   9.00 2 6.25 2.70  
160120811 2.5   9.00 2 6.25 3.45  
160122295 2.0   0.00 5 15.62 0.60  
160122660 10.0   9.00   0.00 5.70  
160141168     0.00 5 15.62 0.00 TR
160146232 4.0   8.20 1 3.12 3.66  
160148260 8.0   9.00   0.00 5.10  
170010481     0.00 8 25.00 0.00 TR
170023591 3.0   7.40 3 9.38 3.12  
170051579     0.00 8 25.00 0.00 TR
170052915 0.0   0.00 11 34.38 0.00 SR
170065154     0.00 8 25.00 0.00 TR
170080846 9.0   9.00 5 15.62 5.40  
170144631 4.0   9.00 4 12.50 3.90  
180046799     0.00 19 59.38 0.00 SR

(*) Última atualização: [2018-06-20 Qua 21:09]

Calendário de aulas

  1. [2018-03-05 Seg] Introdução e Motivação
    1. Leitura complementar (com exercícios!): Indução
  2. [2018-03-07 Qua] Indução estrutural
    1. Seção 1.3, AM17
    2. 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 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. Arquivo PVS: soma
  3. [2018-03-19 Seg 17:56]: Novos exercícios (pvs)
    1. Existe uma tabela de comandos PVS no capítulo 4 das notas de aulas.
  4. [2018-03-12 Seg] Sintaxe da Lógica Proposicional
    1. Seção 1.2, AM17
  5. [2018-03-14 Qua] Dedução Natural na Lógica Proposicional Intuicionista
    1. Seção 1.4, AM17
  6. [2018-03-19 Seg] Dedução Natural na Lógica Proposicional Clássica
    1. Seção 1.4, AM17
  7. [2018-03-21 Qua] Exercícios
    1. Local: LINF 2
  8. [2018-03-26 Seg] Semântica da Lógica Proposicional Clássica
    1. Seção 1.5, AM17
  9. [2018-03-28 Qua] Cálculo de sequentes (Caso proposicional)
    1. Seções 3.1 e 3.2, AM17
    2. Exercício PVS: landing_weather
  10. [2018-04-02 Seg] A correção da Lógica Proposicional Clássica
    1. Seção 1.6.1, AM17
  11. [2018-04-04 Qua] A completude da Lógica Proposicional Clássica
    1. Seção 1.6.2, AM17
    2. Local: PAT AT 021
  12. [2018-04-09 Seg] Caracterizações da Lógica Proposicional Clássica
    1. Seção 1.4, AM17
    2. Local: PAT AT 021
  13. [2018-04-11 Qua]
    1. Local: PAT AT 021
  14. [2018-04-16 Seg]
    1. Gabarito da primeira lista de exercícios: pdf
    2. Gabarito da lista de Gentzen: pdf
    3. Local: PAT AT 021
  15. [2018-04-18 Qua] Prova 1 (Gabarito: pdf)
    1. Local: PAT AT 021
  16. [2018-04-23 Seg] Lógica de Primeira Ordem (Dedução Natural)
    1. Local: PAT AT 021
  17. [2018-04-25 Qua] Lógica de Primeira Ordem (Cálculo de Gentzen)
    1. Local: LINF 2 (Pavilhões fechados!)
  18. [2018-04-30 Seg] Semântica da Lógica de Primeira Ordem

    1. Local: PAT AT 021

    [2018-05-02 Qua] Aula cancelada (LINF e pavilhões fechados)

  19. [2018-05-07 Seg] Correção da Lógica de Primeira Ordem
    1. Local: PAT AT 021
  20. [2018-05-09 Qua] Equivalência entre Dedução Natural e Cálculo de Sequentes (Caso intuicionista)
    1. Local: PAT AT 021
  21. [2018-05-14 Seg] Equivalência entre Dedução Natural e Cálculo de Sequentes (Caso clássico)
    1. Local: PAT AT 021
  22. [2018-05-16 Qua] Apresentação do projeto e continuação da equivalência entre Dedução Natural e Cálculo de Sequentes
    1. Local: LINF 2
  23. [2018-05-21 Seg] Completude da LPO e o Projeto (Algoritmo de Ford-Johnson)
    1. Local: PAT AT 021
  24. [2018-05-23 Qua] Projeto: Algoritmo de Ford-Johnson
    1. Local: LINF 2
  25. [2018-05-28 Seg] Mais comentários sobre o Projeto

    1. Local: PAT AT 021

    [2018-05-30 Qua] Aula cancelada

  26. [2018-06-04 Seg] Completude da LPO
    1. Local: PAT AT 021
  27. [2018-06-06 Qua] Mais comentários sobre o Projeto, e exercícios.
    1. Local: PAT AT 021
  28. [2018-06-11 Seg] Apresentação do projeto
    1. Local: PAT AT 021
    2. Todos os grupos devem estar presentes. Se houver necessidade, as apresentações continuarão na aula seguinte.
    3. A ordem de apresentação será definida por sorteio.
  29. [2018-06-13 Qua] Não haverá aula
    1. Estarei disponível para tirar dúvidas.
      1. Local: Sala 03 (prédio CIC/EST)
  30. [2018-06-18 Seg] Indecidibilidade da LPO e exercícios
    1. Local: PAT AT 021
  31. [2018-06-20 Qua] Aula de exercícios
    1. Local: PAT AT 021
  32. [2018-06-25 Seg] Prova 2
    1. Local: PAT AT 021

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

Email: contato@flaviomoura.mat.br

Created: 2018-06-20 Qua 21:09

Validate