117366 - Lógica Computacional 1 (Turma A)

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.
  • A bibliografia principal da disciplina pode ser encontrada no site da Springer ou na Amazon (Amazon BR).
    • 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.
  • [2017-08-24 Thu 14:45]: Primeira lista de exercícios (pdf) (gabarito: pdf)
  • [2017-09-04 Mon 17:57]: Aulas de revisão
    • Estagiário de docência: Thiago Mendonça
    • Local: PJC BT 101
    • Dias: 11, 13 e 18 de setembro/2017
    • Horário: 18h - 19h.
  • [2017-09-18 Mon 17:51]: Gabarito da primeira lista de exercícios (pdf)
  • [2017-09-20 Wed 18:11]: Gabarito da primeira prova (pdf)
  • [2017-10-04 Wed 14:02]: As aulas das quartas-feiras serão realizadas no LINF 4
  • [2017-10-04 Wed 15:26]: Revisão da prova 1: <2017-10-16 Mon 17:00>–<2017-10-16 Mon 18:00> na sala 3 (CIC/EST)
  • [2017-10-10 Tue 10:20]: Projeto do curso
  • [2017-11-07 Tue 10:15]: Segunda lista de exercícios (pdf)
  • [2017-11-20 Mon 14:41]: Aulas de revisão
    • Estagiário de docência: Thiago Mendonça
    • Local: PJC BT 101
    • Dias: 22, 23, 27 e 28 de novembro/2017
    • Horário: 18h - 19h.
  • [2017-11-27 Mon 07:11]: Gabarito da segunda lista de exercícios (pdf)
  • [2017-11-29 Wed 22:37]: Gabarito da segunda prova (pdf)
  • [2017-12-01 Fri 16:28]: Revisão de menção
    • Data e horário: [2017-12-11 Mon 09:00]–[2017-12-11 Mon 11:00]
    • Local: Sala 03 do prédio CIC/EST

Quadro de Notas

Matrícula Grupo Apresentação Relatório Nota Final
130039870 7 7.0 7.0 7.00
140080279 7 7.0 7.0 7.00
140134573 8 10.0 8.0 9.20
140136282       0.00
140136371 8 10.0 8.0 9.20
140160299 4 10.0 7.5 9.00
140166378       0.00
140168915 4 10.0 7.5 9.00
140170961 3 10.0 9.0 9.60
150005539 12 10.0 8.5 9.40
150008023 3 10.0 9.0 9.60
150009887 3 10.0 9.0 9.60
150015747 11 10.0 7.5 9.00
150019343 2 10.0 8.5 9.40
150033699       0.00
150038381 3 10.0 9.0 9.60
150094213 1 8.0 7.0 7.60
150118783 11 10.0 7.5 9.00
150122322 9     0.00
150131992 2 5.0 8.5 6.40
150132662 1 8.0 7.0 7.60
150144482 1 8.0 7.0 7.60
150150296 2 10.0 8.5 9.40
160002575       0.00
160003636 5 10.0 7.5 9.00
160006490 6 10.0 7.0 8.80
160006597 1 8.0 7.0 7.60
160011795 6 10.0 7.0 8.80
160015031 8 10.0 8.0 9.20
160015537 6 10.0 7.0 8.80
160038316 5 10.0 7.5 9.00
160046424 5 10.0 7.5 9.00
160047617 4 10.0 7.5 9.00
160048036       0.00
160058376       0.00
160071569 6 10.0 7.0 8.80
160109990       0.00
160119740       0.00
160138043 10     0.00
160148804       0.00
160166179       0.00
        0.00
Matrícula Prova 1 Prova 2 Média Projeto Faltas(*) Nota Final Menção Faltas (%)
130039870 2.0 0.0 0.86 7.00 4 2.70 II 13.79
140080279 7.0 2.0 4.14 7.00 3 5.00 MM 10.34
140134573 6.0 5.0 5.43 9.20 1 6.56 MM 3.45
140136371 5.0 5.0 5.00 0.00 2 3.50 MM 6.90
140160299 10.0 9.0 9.43 9.20 1 9.36 SS 3.45
140166378 1.0   0.43 9.00 6 3.00 II 20.69
140168915 6.0 7.0 6.57 0.00 1 4.60 MS 3.45
140170961 10.0 6.5 8.00 9.00 3 8.30 MS 10.34
150005539 6.0 4.5 5.14 9.60 6 6.48 MM 20.69
150008023 7.0 4.0 5.29 9.40 1 6.52 MM 3.45
150009887 8.0 9.3 8.74 9.60 3 9.00 SS 10.34
150015747 10.0 10.0 10.00 9.60 3 9.88 SS 10.34
150019343 8.5 6.0 7.07 9.00 2 7.65 MS 6.90
150033699 4.5   1.93 9.40 3 4.17 TR 10.34
150038381 6.0 6.0 6.00 0.00 2 4.20 MS 6.90
150094213 5.0 3.5 4.14 9.60 7 5.78 MM 24.14
150118783 7.0 7.5 7.29 7.60 3 7.38 MS 10.34
150122322 0.0   0.00 9.00 8 2.70 SR 27.59
150131992 10.0 6.0 7.71 0.00 1 5.40 MS 3.45
150132662 2.0 6.0 4.29 6.40 1 4.92 MM 3.45
150144482 0.0   0.00 7.60 1 2.28 II 3.45
150150296 4.5 8.5 6.79 7.60 0 7.03 MS 0.00
160002575 9.0 8.0 8.43 9.40 5 8.72 MM 17.24
160003636 10.0 6.0 7.71 0.00 1 5.40 MS 3.45
160006490 10.0 9.0 9.43 9.00 1 9.30 SS 3.45
160006597 8.5 8.5 8.50 8.80 2 8.59 MS 6.90
160011795 10.0 10.0 10.00 7.60 3 9.28 SS 10.34
160015031 2.5 10.0 6.79 8.80 2 7.39 MS 6.90
160015537 10.0 8.5 9.14 9.20 3 9.16 SS 10.34
160038316 4.0 3.5 3.71 8.80 1 5.24 MM 3.45
160046424 7.5 5.5 6.36 9.00 1 7.15 MS 3.45
160047617 10.0 10.0 10.00 9.00 5 9.70 SS 17.24
160048036     0.00 9.00 4 2.70 TR 13.79
160058376 9.0 9.0 9.00 0.00 5 6.30 MM 17.24
160071569 10.0 5.0 7.14 0.00 1 5.00 MS 3.45
160109990 0.0   0.00 8.80 2 2.64 TR 6.90
160119740     0.00 0.00 1 0.00 TR 3.45
160138043 1.0   0.43 0.00 10 0.30 SR 34.48
160148804 0.0   0.00 0.00 3 0.00 TR 10.34
160166179     0.00 0.00 6 0.00 TR 20.69

(*) Última atualização: [2017-12-12 Tue 09:37]

Calendário de aulas

  1. [2017-08-07 Mon] Motivação e Sintaxe da Lógica Proposicional ✓
    • Primeiras regras de dedução natural. Prove os seguintes sequentes:
      1. \(p \land (q \land r) \vdash (p \land q) \land r\)
      2. \(p \lor (q \lor r) \vdash (p \lor q) \lor r\)
      3. \(p \land (q \lor r) \vdash (p \land q) \lor (p \land r)\)
      4. \(p \lor (q \land r) \vdash (p \lor q) \land (p \lor r)\)
    • Utilize o ProofWeb para verificar suas provas.
  2. [2017-08-09 Wed] Indução estrutural ✓
    • Leitura complementar (com exercícios!): Indução
    • Exercícios sugeridos: Seção 1.3 (exercício 3).
    • Exercícios: 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:

      \[|l| = \left\{\begin{array}{ll} 0, & \mbox{ se } l = nil \\ 1 + |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.\]

      • Prove que o comprimento do resultado de concatenar duas listas \(l_1\) e \(l_2\) é igual a soma dos comprimentos destas listas, i.e. \(|concat(l_1,l_2)| = |l_1| + |l_2|\).
      • Prove que \(concat(l,nil) = l\) para qualquer lista \(l\)
      • Prove que \(concat(concat(l_1,l_2),l_3) = concat(l_1,concat(l_2,l_3))\) para listas \(l_1,l_2,l_3\) quaisquer

      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.\]

      • Prove que \(length(rev(l)) = length(l)\), para qualquer lista l.
      • Prove que \(rev(concat(l_1,l_2)) = concat(rev(l_2), rev(l_1))\) para listas \(l_1, l_2\) quaisquer.
      • Prove que \(rev(rev(l)) = l\) para qualquer lista l.
  3. [2017-08-14 Mon] Lógica Proposicional Intuicionista ✓
    • Exercícios sugeridos: Seção 1.4 (exercícios 4, 5, 7, 8, 12, 13, 14 e 18).
  4. [2017-08-16 Wed] Lógica Proposicional Clássica ✓
    • Exercícios sugeridos: Seção 1.4 (exercícios 6, 9, 10, 11, 15, 16 e 17).
  5. [2017-08-21 Mon] Exercícios em Dedução Natural (DN) ✓
  6. [2017-08-23 Wed] Cálculo de sequentes ✓
  7. [2017-08-28 Mon] Exercícios em Cálculo de sequentes ✓
  8. [2017-08-30 Wed] Correção da Lógica Proposicional Clássica ✓
  9. [2017-09-04 Mon] Completude da Lógica Proposicional Clássica ✓
  10. [2017-09-06 Wed] Completude da Lógica Proposicional Clássica ✓
  11. [2017-09-11 Mon] Exercícios em Dedução Natural ✓
  12. [2017-09-13 Wed] Exercícios em Cálculo de Gentzen ✓
  13. [2017-09-18 Mon] Exercícios ✓
    • Gabarito da lista 1: (pdf)
  14. [2017-09-20 Wed] Prova 1 (Gabarito: pdf) ✓

    [2017-09-25 Mon] ITP, TABLEAUX and FroCoS Conferences

    [2017-09-27 Wed] ITP, TABLEAUX and FroCoS Conferences

  15. [2017-10-02 Mon] Lógica de Predicados (LP) ✓
    • Exercícios sugeridos: Seções 2.2 e 2.3
  16. [2017-10-04 Wed] Introdução ao PVS ✓
    • Local: LINF 4
    • Arquivo: pvs
  17. [2017-10-09 Mon] Cálculo de sequentes na LP ✓
  18. [2017-10-11 Wed] Projeto: Ordenação por inserção binária ✓
    • Local: LINF 4
  19. [2017-10-16 Mon] Equivalência entre o Cálculo de Sequentes (CS) e Dedução Natural (DN) ✓
  20. [2017-10-18 Wed] Projeto: Ordenação por inserção binária ✓

    • Local: LINF 4
    • Para que o PVS possa utilizar a nasalib é necessário fazer o seguinte em um terminal:

      export PATH=$PVS_DIR:$PATH

      export PVS_LIBRARY_PATH=$PVS_DIR/nasalib

    [2017-10-23 Mon] Semana Universitária (Não haverá aula)

    [2017-10-25 Wed] Semana Universitária (Não haverá aula)

  21. [2017-10-30 Mon] Aula cancelada (dedetização do PJC)
  22. [2017-11-01 Wed] Projeto: Ordenação por inserção binária ✓
    • Local: LINF 4
  23. [2017-11-06 Mon] Equivalência entre o Cálculo de Sequentes (CS) e Dedução Natural (DN) ✓
    • Caso clássico.
    • Segunda lista de exercícios (pdf)
  24. [2017-11-08 Wed] Projeto: Ordenação por inserção binária
    • Local: LINF 4
  25. [2017-11-13 Mon] Apresentação do projeto

    • Local: PJC BT 101

    [2017-11-15 Wed] Feriado

  26. [2017-11-20 Mon] Correção da Lógica de Predicados
  27. [2017-11-22 Wed] Completude da Lógica de Predicados
    • Local: PJC BT 101
  28. [2017-11-27 Mon] Completude da Lógica de Predicados
  29. [2017-11-29 Wed] Prova 2 (Gabarito: pdf)
    • Local: PJC BT 101

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

Email: contato@flaviomoura.mat.br

Created: 2017-12-12 Tue 09:58

Validate