117366 - Lógica Computacional 1

Referência principal: cite:AM17.
Bibliografia complementar: cite:HR2004, cite:BBJ02, cite:Bur98, cite:cai83, cite:SMF06, cite:eft84, cite:NK04, cite:dalen08.

1. [X] <2019-03-13 qua 19:00> Introdução e motivação
   
   • Leitura complementar: O Princípio da Indução - Elon Lages Lima (pdf) (Eureka vol. 3)
     
   • Arquivos PVS: exercicio1.pvs exercicio2.pvs
     

   • Resumo da aula:
     

     Iniciamos com uma apresentação da estrutura do curso, de como
     será o processo de avaliação, e datas das provas escritas. A
     parte prática do curso consistirá no desenvolvimento de um
     projeto no assistente de provas PVS
     (http://pvs.csl.sri.com/). Assim, os alunos foram orientados a
     instalar o PVS (versão 6.0) em seus computadores
     pessoais. Deve-se observar que o PVS só funciona em sistemas
     operacionais baseados em unix (macosx e linux, por
     exemplo). Usuários do sistema windows costumam instalar alguma
     máquina virtual para poder usar o PVS.
     

     O ambiente moddle (aprender.ead.unb.br) NÃO será utilizado nesta
     disciplina.
     

     Indução matemática e estrutural será fundamental ao longo de todo
     o curso. Assim, o artigo "O Princípio da Indução" do prof. Elon
     Lages Lima (link acima) foi sugerido como leitura complementar
     sobre o tema.
     

     A abordagem do curso consiste em utilizar a lógica de primeira
     ordem para resolver problemas computacionais. O problema
     selecionado para o projeto deste semestre está relacionado com
     propriedades do algoritmo radix sort (que utilizará mergesort
     como algoritmo auxiliar (estável)). Uma revisão sobre estes
     algoritmos também é recomendável.
     

     A bibliografia principal a ser utilizada é cite:AM17, e uma cópia
     deste material encontra-se disponível na pasta 22 da copiadora
     Exata (final da ala norte do ICC). Alternativamente, este
     material pode ser comprado online a partir dos links: Springer,
     Amazon.com, Amazon.com.br
     

     Por fim, dois problemas simples foram propostos para serem
     resolvidos antes da próxima aula:
     

     1. Prove que para todo natural \( n \) vale a seguinte igualdade:
        \( \displaystyle\sum_{i=0}^n i = \frac{n.(n+1)}{2} \)
        
     2. Prove que a soma dos \( n \) primeiros números ímpares é igual
        a \( n^2 \).
        

     Resolva estes 2 problemas para revisar indução matemática porque
     na próxima aula veremos como estas provas podem ser feitas no
     PVS. Para seguir a construção da prova em PVS é fundamental que
     os exercícios tenham sido resolvidos anteriormente em papel e
     lápis. Não deixe de resolvê-los!
     

2. [X] <2019-03-18 seg 19:00> Indução estrutural
   

   • 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.
        
   • Arquivo PVS: exercicio3.pvs
     

   • Resumo da aula:
     

     Resolvemos o primeiro dos problemas propostos na última aula:
     

     • Prove que para todo natural \( n \) vale a seguinte igualdade:
       \( \displaystyle\sum_{i=0}^n i = \frac{n.(n+1)}{2} \)
       

     Em seguida, a prova foi feita no PVS seguindo os mesmos passos da
     solução apresentada no quadro. O problema 1 envolvendo listas
     também foi resolvido da mesma forma (no quadro e no PVS).
     

     Os comandos de prova do PVS utilizados nestes exercícios foram
     basicamente os seguintes:
     

     1. Para iniciar uma prova: M-x prove ou M-x x-prove.
        

        Lembre-se que o cursos deve estar posicionado na propriedade
        que se deseja provar.
        

     2. (induct "n") : iniciar a prova utilizando indução em n.
        
     3. (skeep): fórmulas universais no consequente, ou existenciais
        no antecedente.
        
     4. (inst i "a"): instancia o primeiro quantificador da fórmula
        i (universal no antecedente, ou existencial no consequente)
        com o termo a.
        
     5. (expand "def" i (n1 n2 ... nk)): aplica a definição def
        nas ocorrências n1, n2, ..., nk da fórmula i. Se os
        argumentos i e (n1 n2 ... nk) não forem fornecidos, todas
        as ocorrências de def serão substituídas.
        
     6. (replace i j): Se a fórmula i for uma igualdade da forma
        \(A = B\) então todas as ocorrências de \(A\) na fórmula j
        são substituídas por \(B\).
        
     7. (assert): Realiza todas as simplificações possíveis.
        

     Como sugestão, prove todos os lemas que estão nos arquivos
     exercicio1.pvs, exercicio2.pvs e exercicio3.pvs.
     

     Faça a leitura das seções 1.1, 1.2, 1.3 e 1.4 do Capítulo 1 das
     notas de aula (cite:AM17) porque este será o assunto da próxima
     aula!
     

3. [X] <2019-03-20 qua 19:00> Lógica Proposicional Intuicionista (LPI)
   
   • Leitura: Capítulo 1 (até seção 1.4 inclusive), cite:AM17
     
     • Exercícios propostos: 1-4, 7, 8, 12, 13, 14, 18.
       
     • Resumo da aula: Foi feita uma introdução do sistema de
       dedução natural para a lógica proposicional intuicionista, e
       alguns exemplos.
       
4. [X] <2019-03-25 seg 19:00> Lógica Proposicional Intuicionista (LPI)
   
   • Resumo da aula: Aula de exercícios.
     
5. [X] <2019-03-27 qua 19:00> Lógica Proposicional Clássica (LPC)
   
   • Leitura: Capítulo 1 (até seção 1.4 inclusive), cite:AM17
     
     • Exercícios: 5,6,9-11,15-17.
       
     • Resumo da aula: Exercícios e apresentação da lógica
       proposicional clássica. Resolver todos os exercícios propostos
       nas notas de aula até a Seção 1.4 (inclusive).
       
6. [X] <2019-04-01 seg 19:00> Semântica da LPC
   
   • Resumo da aula: Foi apresentada a semântica da lógica
     proposicional clássica (Seção 1.5 das notas de aula).
     
7. [X] <2019-04-03 qua 19:00> Correção da LPC
   
   • Resumo da aula: Foi apresentada a estrutura da prova de
     correção da lógica proposicional clássica. Dois dos sete casos
     foram feitos em detalhes (introdução da conjunção e prova por
     contradição). Os outros casos foram deixados como exercícios.
     
8. [X] <2019-04-08 seg 19:00> Completude da LPC
   
   • Resumo da aula: Foi apresentada a ideia geral a prova do
     teorema da completude da lógica proposicional clássica.
     
9. [X] <2019-04-10 qua 19:00> Aula de exercícios
   
   • Resumo da aula: Provamos que no fragmento negativo da lógica
     proposicional, uma fórmula qualquer e sua dupla negação são
     equivalentes (exercício 14 das notas de aula).
     
10. [X] <2019-04-15 seg 19:00> Projeto em PVS:
    
    • Resumo da aula: Comentários sobre o projeto (radix sort), e
      resolução de exercícios sobre listas de naturais em PVS.
      
11. [X] <2019-04-17 qua 19:00> ordenação por inserção no PVS: (pvs)
    
    • Resumo da aula: Um exercício envolvendo instanciar a lei de
      Peirce foi resolvido. Iniciamos a resolução do arquivo pvs
      anexo.
      
12. [X] <2019-04-22 seg 19:00> Aula de Revisão
    
    • Resumo da aula: Resolução de exercícios.
      
13. [X] <2019-04-24 qua 19:00> Primeira Prova
    
    1. Gabarito (pdf)
       
14. [X] <2019-04-29 seg 19:00> Introdução ao Cálculo de Sequentes (CS)
    
    • Resumo da aula: Foi introduzido o cálculo de sequentes
      conforme capítulo 3 das notas de aulas, incluindo alguns
      exemplos.
      
    • [2019-05-01 qua] Feriado
      
15. [X] <2019-05-06 seg 19:00> Introdução à Lógica de Predicados (LP)
    
    • Resumo da aula: Foi apresentada a gramática da lógica de
      predicados, assim como as regras (em dedução natural e cálculo
      de sequentes) envolvendo os quantificadores.
      
16. [X] <2019-05-08 qua 19:00> Aula de exercícios
    
17. [X] <2019-05-13 seg 19:00> Comentários sobre o projeto.
    
    • Resumo da aula: Foram feitos comentários gerais sobre o
      projeto, e sobre o PVS. Alguns exemplos baseados em um curso
      realizado na NASA em 2012 foram utilizados (Link para a página do curso). Arquivos do curso: files/lc1/pvsclass2012.tgz
      
    • [2019-05-15 qua 19:00] Não haverá aula: Mobilização Nacional pela Educação (Museu da República, 10h).
      
18. [X] <2019-05-20 seg 19:00> Correção da lógica de predicados
    
    • Resumo da aula: Foi apresentada apresentada a ideia geral da
      prova indutiva da correção da lógica de predicados. O caso em
      que a última regra da derivação corresponde à introdução do
      quantificador universal foi discutido em detalhes.
      
19. [X] <2019-05-22 qua 19:00> Discussão do projeto
    
    • Resumo da aula: A partir de uma definição recursiva da
      propriedade de ordenação de listas (de naturais), mostramos em
      PVS que a função isort retorna sempre uma lista ordenada como
      resultado. Arquivo PVS: files/IS2019-1.pvs
      
20. [X] <2019-05-27 seg 19:00> CS versus DN
    
    • Resumo da aula: Foram feitos comentários sobre o projeto, e
      apresentada a ideia geral da equivalência, a ser demonstrada,
      entre o Cálculo de Sequentes (CS) e o sistema de Dedução Natural
      (DN).
      
21. [X] <2019-05-29 qua 19:00> CS versus DN (caso intuicionista)
    
    • Resumo da aula: Foram feitos comentários sobre a questão 1 do
      projeto, e apresentado o esboço da prova de como uma prova
      intuicionista no cálculo de Gentzen pode ser transformada em uma
      prova intuicionista em dedução natural.
      
    • Segunda lista de exercícios (pdf)
      
22. [X] <2019-06-03 seg 19:00> CS versus DN (caso clássico)
    
    • Resumo da aula: Completamos a ideia da prova da equivalência
      entre o Cálculo de Sequentes e Dedução Natural para o caso
      intuicionista, e iniciamos a generalização para o caso clássico.
      
23. [X] <2019-06-05 qua 19:00> CS versus DN (caso clássico)
    
    • Resumo da aula: Apresentamos a ideia geral da prova de
      equivalência entre o Cálculo de Sequentes e o sistema de Dedução
      Natural para a Lógica de Predicados Clássica. Estas ideias
      também se encontram nas notas de aulas do curso.
      
24. [X] <2019-06-10 seg 19:00> Apresentação do projeto
    
    • No início da aula definiremos a ordem de apresentação dos
      grupos. Grupos ausentes nesta aula ficarão sem nota de
      apresentação.
      
    • [2019-06-12 qua 19:00] Aula cancelada: Devido a um problema de
      ordem pessoal, a aula foi cancelada.
      
25. [X] <2019-06-17 seg 19:00> Completude da LPO
    
    • [2019-06-19 qua 19:00] Aula cancelada
      
26. [X] <2019-06-24 seg 19:00> Aula de exercícios
    
27. [X] <2019-06-26 qua 19:00> Aula de exercícios
    
28. [ ] <2019-07-01 seg 19:00> Segunda Prova
    

• State "DONE" from "WAITING" [2019-03-12 ter 17:32]
  
• State "WAITING" from "PROGRESS" [2019-03-12 ter 11:34]
  Aguardando retorno do Mauricio
  
• State "PROGRESS" from "TODO" [2019-03-06 qua 19:21]
  preparando o cronograma
  

(*) Última atualização: [2019-07-08 seg 09:28]