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)
    • Dia e horário: Todas as quintas de 12h às 13h
    • Local: PAT AT 044 (a partir de [2017-03-30 Qui])
  • 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)

Quadro de Notas

Matrícula Grupos [2017-01-03 Ter] [2017-01-05 Qui] Apresentação Relatório Nota Final Arquivos
100123571              
110012496              
110024702              
110028384              
110148746              
120125471              
120129647              
120151898              
130024902              
140030395              
140083162              
140135910              
140142959              
140145621              
140156429              
140159932              
150004354              
150009101              
150014961              
150015585              
150048718              
150124236              
150126158              
150126808              
150141661              
150146612              
160008981              
160014522              
160113121              
160116929              
160123283              
160125260              
160127815              
160141575              
160146712              
170037100              
170080846              
Matrícula Prova 1 Prova 2 Média das provas Projeto Faltas(*) Faltas (%) Nota Final Menção
100123571 1.5   0.64285714 0   0 0.45  
110012496     0 0   0 0  
110024702 8.5   3.6428571 0   0 2.55  
110028384 1.5   0.64285714 0   0 0.45  
110148746 2.0   0.85714286 0   0 0.6  
120125471 3.5   1.5 0   0 1.05  
120129647 0.5   0.21428571 0   0 0.15  
120151898 1.0   0.42857143 0   0 0.3  
130024902 0.0   0. 0   0 0.  
140030395 10.0   4.2857143 0   0 3.  
140083162 3.5   1.5 0   0 1.05  
140135910 5.5   2.3571429 0   0 1.65  
140142959 2.0   0.85714286 0   0 0.6  
140145621 1.0   0.42857143 0   0 0.3  
140156429     0 0   0 0  
140159932     0 0   0 0  
150004354 2.0   0.85714286 0   0 0.6  
150009101 7.5   3.2142857 0   0 2.25  
150014961 5.0   2.1428571 0   0 1.5  
150015585 4.5   1.9285714 0   0 1.35  
150048718 5.0   2.1428571 0   0 1.5  
150124236 3.5   1.5 0   0 1.05  
150126158 2.0   0.85714286 0   0 0.6  
150126808 9.0   3.8571429 0   0 2.7  
150141661 8.0   3.4285714 0   0 2.4  
150146612 7.0   3. 0   0 2.1  
160008981     0 0   0 0  
160014522 2.5   1.0714286 0   0 0.75  
160113121 6.5   2.7857143 0   0 1.95  
160116929     0 0   0 0  
160123283 1.0   0.42857143 0   0 0.3  
160125260 0.5   0.21428571 0   0 0.15  
160127815 4.5   1.9285714 0   0 1.35  
160141575 2.0   0.85714286 0   0 0.6  
160146712     0 0   0 0  
170037100     0 0   0 0  
170080846 1.5   0.64285714 0   0 0.45  
Média 3.8793103   1.5960591     0    

(*) Última atualização: [2017-04-19 Qua 11:45]

Calendário de aulas

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

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

  • Dedução Natural

<2017-03-14 Ter 10:00>–<2017-03-14 Ter 11:50> 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> 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> 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> 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> Exercícios de DN ✓

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

<2017-04-04 Ter 10:00>–<2017-04-04 Ter 11:50> 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> 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> Completude da Lógica Proposicional Clássica ✓

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

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

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

  • Termos, Fórmulas e Substituição

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

  • Teoria da Prova na Lógica de Predicados

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

  • Aula no LINF 4: Exercícios de indução no PVS

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

Email: flaviomoura@unb.br

Created: 2017-04-19 Qua 11:55

Validate