117366 - Lógica Computacional 1

Table of Contents

Quadro de avisos:

[2019-05-20 Seg 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 Qui 16:35]: Gabarito da prova 1 (pdf)

[2019-04-03 Qua 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 Qua 08:44]: Primeira lista de exercícios (pdf)

[2019-04-20 Sáb 22:44]: Gabarito (pdf)

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

Cronograma de aulas [63%]

Referência principal: AM17.
Bibliografia complementar: HR2004, BBJ02, Bur98, cai83, SMF06, eft84, NK04, 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 é 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 (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), 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), 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. [ ] <2019-05-27 Seg 19:00> CS versus DN
  21. [ ] <2019-05-29 Qua 19:00> Exercícios em DN e CS
  22. [ ] <2019-06-03 Seg 19:00> Completude da LP
  23. [ ] <2019-06-05 Qua 19:00> Indecidibilidade da LP
  24. [ ] <2019-06-10 Seg 19:00> Apresentação do projeto
  25. [ ] <2019-06-12 Qua 19:00> Apresentação do projeto
  26. [ ] <2019-06-17 Seg 19:00> Aula de exercícios
  27. [ ] <2019-06-19 Qua 19:00> Aula de exercícios
  28. [ ] <2019-06-24 Seg 19:00> Aula de exercícios
  29. [ ] <2019-06-26 Qua 19:00> Aula de exercícios
  30. [ ] <2019-07-01 Seg 19:00> Segunda Prova

Bibliography

  • [AM17] Ayala-Rincón & de Moura, Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs, Springer (2017).
  • [Pereira15] Wansing, Dag Prawitz on Proofs and Meaning, Springer Publishing Company, Incorporated (2016).
  • [lifehenkin] The Life and Work of Leon Henkin, Springer International Publishing (2014).
  • [dalen08] van Dalen, Logic and structure (4. ed.), Springer (2008).
  • [Sorensen06] S\orensen & Urzyczyn, Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics), Elsevier Science Inc. (2006).
  • [HR2004] Huth & Ryan, Logic in Computer Science: Modelling and Reasoning About Systems, Cambridge University Press (2004).
  • [eft84] Ebbinghaus, , Flum, & Thomas, Mathematical logic, Springer (1984).
  • [epstein90] Epstein, The Semantic Foundations of Logic, Springer Science + Business Media (1990).
  • [2016arXiv160207608M] Moot & Retor\'e, Classical logic and intuitionistic logic: equivalent formulations in natural deduction, G$\backslash$``odel-Kolmogorov-Glivenko translation, ArXiv e-prints, (2016).
  • [lewis1912] LEWIS, Iv.-implication AND THE Algebra OF Logic, Mind, XXI(84), 522-531 (1912). link. doi.
  • [weir15] WEIR, Informal Proof, Formal Proof, Formalism, The Review of Symbolic Logic, 9(01), 23-43 (2015). link. doi.
  • [maierrTN] @BookletmaierrTN, title = Teoria dos N\'umeros, author = R. Maier, year = 2005, note = Available at \tt http://www.mat.unb.br/~maierr/tnotas.pdf
  • [maierrA1] @BookletmaierrA1, title = \'Algebra I, author = R. Maier, year = 2005, note = Available at \tt http://www.mat.unb.br/~maierr/anotas.pdf
  • [bd05] @Miscbd05, author = N. Bezhanishvili and D. de Jongh, title = Intuitionistic Logic, howpublished = \tt http://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf, year = 2005
  • [jz13] de Jongh, & Zhao, Positive Formulas in Intuitionistic and Minimal Logic, 175-189, in in: Logic, Language, and Computation - 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers, edited by (2013)
  • [AM14] Ayala-Rinc\'on & de Moura, Fundamentos da Programa\cc\~ao L\'ogica e Funcional - O princ\'ipio de Resolu\cc\~ao e a Teoria de Reescrita, Universidade de Bras\'ilia (2014).
  • [TroelstraBasicProofTheory] Troelstra & Schwichtenberg, Basic Proof Theory, CUP (2000).
  • [Dyb12] Dybjer, Lindström, Palmgren & Sundholm , Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-L\"of, Springer Nature (2012).
  • [2016arXiv161109473R] Ragde, Proust: A Nano Proof Assistant, ArXiv e-prints, (2016).
  • [caldwell13_struc_induc_princ_funct_progr] Caldwell, Structural Induction Principles for Functional Programmers, CoRR, (2013). link.
  • [BBJ02] Boolosd, Burgess & Jeffrey Richard, Computability and Logic: 4th Ed., Cambridge University Press (2002).
  • [Bur98] Burris, Logic for Mathematics and Computer Science, Prentice Hall (1998).
  • [cai83] Caicedo, Elementos de logica y calculabilidad, Universidad de los Andes, Departamento de Matematicas (1983).
  • [SMF06] da Silva, de Melo & Finger, L\'ogica para computa\cc\~ao, THOMSON PIONEIRA (2006).
  • [NK04] Nederpelt & Kamareddine, Logical Reasoning: A First Course, King's College Publications (2004).

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

  • 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

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 Qua]
  • Segunda prova: [2019-07-01 Seg]

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 Nome completo Prova 1 Prova 2 Apr Rel Projeto Faltas (*) Faltas(%) Nota Final Menção
130110728 Flavio Amaral e Silva 0.0         1 3.33 0.00  
130112267 Geraldino Antonio da Silva 1.5         1 3.33 0.45  
140161741 Rogerio da Rocha Feitoza 0.0         6 20.00 0.00  
140164049 Thiago Santana Marques 0.5         2 6.67 0.15  
150126298 Gabriel dos Santos Martins 3.0         1 3.33 0.90  
160060346 Rafael Martins Diniz 1.0         2 6.67 0.30  
160070431 Fillype Alves do Nascimento 9.0         3 10.00 2.70  
160116821 Daniel Carvalho Moreira           7 23.33 0.00  
160117925 Diego Vaz Fernandes 4.0         2 6.67 1.20  
160127670 João Victor Cabral de Melo 8.5           0.00 2.55  
160133661 Lucas Mariano Carvalho           4 13.33 0.00  
160135478 Marcelo Gonçalves de Sousa Junior           4 13.33 0.00  
160147140 Victor Alves de Carvalho 2.0           0.00 0.60  
160148294 Vitor Hideki Hokino           3 10.00 0.00  
170009840 Felipe Gomes Paradas +2 10.0         1 3.33 3.00  
170010988 Gabriella Tavares Peixoto 0.0         4 13.33 0.00  
170031560 Daniel Lamounier Alves           6 20.00 0.00  
170032990 Erik Bernardo Brito 8.0         2 6.67 2.40  
170038963 Leonardo Ribas do Nascimento +0.5 10.0         3 10.00 3.00  
170102289 Eduardo Ferreira de Assis 8.5           0.00 2.55  
170103544 Gabriel Müller Alexandre de Albuquerque +2 10.0           0.00 3.00  
170109071 Lucas Veríssimo Botelho 6.0         2 6.67 1.80  
170123154 Victor Carneiro Seidel 4.5           0.00 1.35  
170126021 João Pedro Saderi da Silva 1.0           0.00 0.30  
170126021 João Pedro Saderi da Silva             0.00 0.00  
170138585 Bruno Oliveira Gomes 2.0           0.00 0.60  
170140008 Danilo Felix de Castro Pereira 0.0         2 6.67 0.00  
170143970 Guilherme Mendel de Almeida Nascimento 8.0         2 6.67 2.40  
170149668 Lucas Mendonça Macedo Amaral 6.0         1 3.33 1.80  
170153657 Paulo Alvim Alvarenga +1 10.0         3 10.00 3.00  
180012053 Amanda Augusto da Silva 9.0           0.00 2.70  
180013688 Artur de Meira Rodrigues 7.0         2 6.67 2.10  
180029789 Allann Gois Hoffmann 2.0         1 3.33 0.60  
180111515 Hanniel Fernando Lopes Saldanha           8 26.67 0.00  
180147358 Italo Marcos Brandao 6.5         3 10.00 1.95  
  Média 4.93           0.00 1.48  
140132163 Brando Franco de Souza do Lago           9 30.00 0.00 SR
150136986 Lucas Cruz Torreao           18 60.00 0.00 SR
170137058 Andre Bonifacio dos Santos Junior           11 36.67 0.00 SR
170148840 Leonardo Soares Silva           9 30.00 0.00 SR
180033921 Jonas Fernandes da Silva           10 33.33 0.00 TR
180074598 Bernardo Rego Feitosa           1 3.33 0.00 TR
170080641 Salomao Lemos Mosti           6 20.00 0.00 RT
170104630 Gustavo Einstein Soares Oliveira           2 6.67 0.00 RT
120044749 Brandon Araujo Dias             0.00 0.00 RT

(*) Última atualização: [2019-05-24 Sex 09:48]

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

Email: contato@flaviomoura.mat.br

Created: 2019-05-24 Sex 09:48

Validate