117366 - Lógica Computacional 1

Table of Contents

Quadro de avisos:

[2019-07-11 Thu 19:05]: A revisão de menção poderá ser feita amanhã, dia 12, das 13h às 15h, na sala 03 do prédio CIC/EST.

[2019-07-11 Thu 11:28]: Gabarito da prova 2 (pdf)

[2019-07-09 Tue 18:37]: A revisão de menção poderá ser feita até sexta-feira, dia 12. Solicite agendamento de um horário pelo email contato@flaviomoura.mat.br

[2019-06-26 Wed 15:59]: Gabarito da lista 2 (pdf)

[2019-06-12 Wed 09:48]: Devido a um problema de ordem pessoal a aula de hoje está cancelada.

[2019-05-30 Thu 09:21]: Segunda lista de exercícios (pdf)

[2019-05-20 Mon 23:01]: Após a aula de hoje, houve uma breve discussão sobre os teoremas da incompletude de Gödel, e foram solicitadas leituras sobre o tema. Seguem algumas sugestões:

  1. Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. Torkel Franzén;
  2. Gödel's Proof. Ernest Nagel and James Newman;
  3. Godel, Escher, Bach: An Eternal Golden Braid. Douglas R. Hofstadter.

[2019-04-25 Thu 16:35]: Gabarito da prova 1 (pdf)

[2019-04-03 Wed 23:32]: Projeto (pdf) (pvs)

Ao clicar no link do projeto você será direcionado para uma página do Github contendo os grupos criados até o momento.

Clique no grupo que deseja participar (máximo de 3 membros!), ou

Clique em +Create team para criar um novo grupo.

Uma vez que você foi adicionado a um grupo, ou uma vez que você tenha criado um novo grupo esta operação não poderá ser desfeita! Assim, tenham os grupos organizados antes de clicar no link a seguir: link para o projeto.

[2019-04-03 Wed 08:44]: Primeira lista de exercícios (pdf)

[2019-04-20 Sat 22:44]: Gabarito (pdf)

[2019-03-27 Wed 13:15]: Sugestão de leitura: link

Cronograma de aulas [96%]

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

  1. [X] <2019-03-13 Wed 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 é 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 Mon 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 (AM17) porque este será o assunto da próxima
      aula!

  3. [X] <2019-03-20 Wed 19:00> Lógica Proposicional Intuicionista (LPI)
    • Leitura: Capítulo 1 (até seção 1.4 inclusive), 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 Mon 19:00> Lógica Proposicional Intuicionista (LPI)
    • Resumo da aula: Aula de exercícios.
  5. [X] <2019-03-27 Wed 19:00> Lógica Proposicional Clássica (LPC)
    • Leitura: Capítulo 1 (até seção 1.4 inclusive), 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 Mon 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 Wed 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 Mon 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 Wed 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 Mon 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 Wed 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 Mon 19:00> Aula de Revisão
    • Resumo da aula: Resolução de exercícios.
  13. [X] <2019-04-24 Wed 19:00> Primeira Prova
    1. Gabarito (pdf)
  14. [X] <2019-04-29 Mon 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 Wed] Feriado
  15. [X] <2019-05-06 Mon 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 Wed 19:00> Aula de exercícios
  17. [X] <2019-05-13 Mon 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 Wed 19:00] Não haverá aula: Mobilização Nacional pela Educação (Museu da República, 10h).
  18. [X] <2019-05-20 Mon 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 Wed 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 Mon 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 Wed 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 Mon 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 Wed 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 Mon 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 Wed 19:00] Aula cancelada: Devido a um problema de
      ordem pessoal, a aula foi cancelada.
  25. [X] <2019-06-17 Mon 19:00> Completude da LPO
    • [2019-06-19 Wed 19:00] Aula cancelada
  26. [X] <2019-06-24 Mon 19:00> Aula de exercícios
  27. [X] <2019-06-26 Wed 19:00> Aula de exercícios
  28. [ ] <2019-07-01 Mon 19:00> Segunda Prova

DONE Plano de Ensino - 2019/1 (Turma B)

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

Objetivos

  • Compreender os fundamentos da lógica proposicional clássica e
    da lógica de predicados;
  • Compreender diferentes métodos de validação de teoremas e
    programas.

Metodologia de ensino e critérios de avaliação

O conteúdo será abordado em aulas expositivas nas quais serão
fornecidos conceitos teóricos e aplicados. Questões técnicas da
matéria serão respondidas em horário de aula, ou por e-mail. Questões
administrativas não serão resolvidas por e-mail.

Serão realizadas 2 (duas) avaliações escritas \(P_1\) e \(P_2\) com pesos
3.0 e 4.0, respectivamente; e um projeto com implementação com peso
3.0. A média final \(MF\) é dada por:

\[ MF = \displaystyle \frac{3.P_1 + 4.P_2 + 3.Prj}{10} \]

Para ser aprovado, o aluno deve cumprir simultaneamente os seguintes itens:

  • Frequência igual ou superior a 75% nas aulas,
  • \(MF \geq 5\).

A menção final é definida como a seguir:

Menção Nota
SS (Superior) 9.0 – 10.0
MS (Médio Superior) 7.0 - 8.9
MM (Médio) 5.0 - 6.9
MI (Médio Inferior) 3.0 - 4.9
II (Inferior) 0.1 - 2.9
SR (Sem Rendimento) 0.0 ou mais de 25% de faltas

Data das provas

  • Primeira prova: [2019-04-24 Wed]
  • Segunda prova: [2019-07-01 Mon]

Projeto

Um projeto de especificação e prova de algoritmos e/ou teorias
algébricas utilizando um assistente de prova baseado em lógica será
desenvolvido ao longo do semestre. Os detalhes do projeto serão
fornecidos posteriormente.

Conteúdo Programático

  1. Noções Básicas
    1. Linguagem Natural vs Linguagens Formais;
    2. Verdade, Validade, Satisfatibilidade;
    3. Lógica Proposicional: Sintaxe e Semântica, Propriedades e Relações Semânticas, Consequência Lógica e Simplificação de Fórmulas;
    4. Lógica de Primeira Ordem: Sintaxe e Semântica, Propriedades e Relações Semânticas;
    5. Formas Normais.
  2. Métodos de Validação
    1. Métodos Diretos de Prova;
    2. Métodos de Prova por Contradição;
    3. Indução.
  3. Linguagens para experimentação
    1. Aplicações básicas.

Quadro de Notas:

Matrícula Prova 1 Prova 2 Apr Rel Projeto Faltas (*) Faltas(%) Nota Final Menção
130110728 0.0 0.0 4.0 6.0 4.80 2 6.67 1.44 II
130112267 1.5 1.0 4.0 6.0 4.80 3 10.00 2.29 II
140164049 0.5 0.0 4.0 6.0 4.80 6 20.00 1.59 II
150126298 3.0 1.5 5.0 5.0 5.00 1 3.33 3.00 MI
160070431 9.0 3.0 10.0 6.0 8.40 6 20.00 6.42 MM
160117925 4.0 6.5 5.0 5.0 5.00 4 13.33 5.30 MM
160127670 8.5 2.5 10.0 6.0 8.40   0.00 6.07 MM
160133661         0.00 4 13.33 0.00 II
160135478         0.00 4 13.33 0.00 II
160147140 2.0 1.5 7.0 5.0 6.20 1 3.33 3.06 MI
160148294         0.00 3 10.00 0.00 II
170009840 10.0 9.0 10.0 6.0 8.40 3 10.00 9.12 SS
170032990 8.0 4.0     0.00 7 23.33 4.00 MI
170038963 10.0 5.5 7.0 6.0 6.60 6 20.00 7.18 MS
170102289 8.5 6.5 8.0 7.0 7.60   0.00 7.43 MS
170103544 10.0 10.0     0.00 1 3.33 7.00 MS
170109071 6.0 7.5 7.5 4.0 6.10 3 10.00 6.63 MM
170123154 4.5 8.5 7.5 4.0 6.10 1 3.33 6.58 MM
170126021 1.0       0.00 1 3.33 0.30 II
170138585 2.0       0.00 7 23.33 0.60 II
170140008 0.0 0.0     0.00 4 13.33 0.00 II
170143970 8.0 8.5 8.0 7.0 7.60 3 10.00 8.08 MS
170149668 6.0 7.0 7.5 4.0 6.10 2 6.67 6.43 MM
170153657 10.0 6.0 8.0 7.0 7.60 5 16.67 7.68 MS
180012053 9.0 4.0 7.0 6.0 6.60 1 3.33 6.28 MM
180013688 7.0 7.0 5.5 4.0 4.90 3 10.00 6.37 MM
180029789 2.0 0.0 5.5 4.0 4.90 2 6.67 2.07 II
180147358 6.5 1.5 7.0 5.0 6.20 4 13.33 4.41 MI
  4.89   6.88 8.38 7.11   0.00 3.60  
160060346 1.0       0.00 8 26.67 0.30 SR
170010988 0.0       0.00 8 26.67 0.00 SR
140161741 0.0       0.00 9 30.00 0.00 SR
170031560         0.00 8 26.67 0.00 SR
180111515         0.00 8 26.67 0.00 SR
160116821         0.00 8 26.67 0.00 SR
140132163         0.00 9 30.00 0.00 SR
150136986         0.00 18 60.00 0.00 SR
170137058         0.00 11 36.67 0.00 SR
170148840         0.00 9 30.00 0.00 SR
180033921         0.00 10 33.33 0.00 TR
180074598         0.00 1 3.33 0.00 TR
170080641         0.00 6 20.00 0.00 RT
170104630         0.00 2 6.67 0.00 RT
120044749         0.00   0.00 0.00 RT

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

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

Email: contato@flaviomoura.mat.br

Created: 2019-07-11 Thu 19:51

Validate