117366 - Lógica Computacional 1

Table of Contents

Quadro de avisos:

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.

Cronograma de aulas [6%]

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

  1. [X] [2019-03-13 Qua] 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] 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. [ ] [2019-03-20 Qua] Lógica Proposicional Intuicionista (LPI)
    • Leitura: Capítulo 1 (até seção 1.4 inclusive), AM17
      • Exercícios: 1-4, 7, 8, 12, 13, 14, 18.
  4. [ ] [2019-03-25 Seg] 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.
  5. [ ] [2019-03-27 Qua] Exercícios em Dedução Natural (DN)
  6. [ ] [2019-04-01 Seg] Semântica da LPC
  7. [ ] [2019-04-03 Qua] Correção da LPC
  8. [ ] [2019-04-08 Seg] Completude da LPC
  9. [ ] [2019-04-10 Qua] Dedução à la Gentzen (CS)
  10. [ ] [2019-04-15 Seg] Exercícios de derivação em CS
  11. [ ] [2019-04-17 Qua] Exercícios de derivação em DN e CS
  12. [ ] [2019-04-22 Seg] Aula de Revisão
  13. [ ] [2019-04-24 Qua] Primeira Prova
  14. [ ] [2019-04-29 Seg] Lógica de Predicados (LP) em DN
    • [2019-05-01 Qua] Feriado
  15. [ ] [2019-05-06 Seg] Exercícios em DN
  16. [ ] [2019-05-08 Qua] Exercícios em DN
  17. [ ] [2019-05-13 Seg] Correção da LP
  18. [ ] [2019-05-15 Qua] Lógica de Predicados (LP) em CS
  19. [ ] [2019-05-20 Seg] CS versus DN
  20. [ ] [2019-05-22 Qua] CS versus DN
  21. [ ] [2019-05-27 Seg] Exercícios em DN e CS
  22. [ ] [2019-05-29 Qua] Exercícios em DN e CS
  23. [ ] [2019-06-03 Seg] Completude da LP
  24. [ ] [2019-06-05 Qua] Indecidibilidade da LP
  25. [ ] [2019-06-10 Seg] Apresentação do projeto
  26. [ ] [2019-06-12 Qua] Apresentação do projeto
  27. [ ] [2019-06-17 Seg] Aula de exercícios
  28. [ ] [2019-06-19 Qua] Aula de exercícios
  29. [ ] [2019-06-24 Seg] Aula de exercícios
  30. [ ] [2019-06-26 Qua] Aula de exercícios
  31. [ ] [2019-07-01 Seg] 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).

Quadro de Notas:

  Matrícula Grupo Apresentação Relatório Nota Final
1 120044749        
2 130110728        
3 130112267        
4 140132163        
5 140161741        
6 140164049        
7 150126298        
8 150136986        
9 160060346        
10 160070431        
11 160116821        
12 160117925        
13 160127670        
14 160133661        
15 160135478        
16 160147140        
17 160148294        
18 170009840        
19 170010988        
20 170031560        
21 170032990        
22 170038963        
23 170080641        
24 170102289        
25 170103544        
26 170104630        
27 170123154        
28 170137058        
29 170138585        
30 170140008        
31 170148840        
32 170153657        
33 180012053        
34 180013688        
35 180029789        
36 180033921        
37 180074598        
38 180111515        
39 180147358        
          0.00
  Matrícula Prova 1 Prova 2 Projeto Faltas(*) Faltas (%) Nota Final Menção
1 120044749     0.00 1 3.23 0.00  
2 130110728     0.00   0.00 0.00  
3 130112267     0.00   0.00 0.00  
4 140132163     0.00   0.00 0.00  
5 140161741     0.00   0.00 0.00  
6 140164049     0.00   0.00 0.00  
7 150126298     0.00   0.00 0.00  
8 150136986     0.00 2 6.45 0.00  
9 160060346     0.00 1 3.23 0.00  
10 160070431     0.00   0.00 0.00  
11 160116821     0.00   0.00 0.00  
12 160117925     0.00   0.00 0.00  
13 160127670     0.00   0.00 0.00  
14 160133661     0.00   0.00 0.00  
15 160135478     0.00   0.00 0.00  
16 160147140     0.00   0.00 0.00  
17 160148294     0.00   0.00 0.00  
18 170009840     0.00   0.00 0.00  
19 170010988     0.00   0.00 0.00  
20 170031560     0.00   0.00 0.00  
21 170032990     0.00 1 3.23 0.00  
22 170038963     0.00   0.00 0.00  
23 170080641     0.00 2 6.45 0.00  
24 170102289     0.00   0.00 0.00  
25 170103544     0.00   0.00 0.00  
26 170104630     0.00   0.00 0.00  
27 170123154     0.00   0.00 0.00  
28 170137058     0.00 1 3.23 0.00  
29 170138585     0.00   0.00 0.00  
30 170140008     0.00   0.00 0.00  
31 170148840     0.00 2 6.45 0.00  
32 170153657     0.00 1 3.23 0.00  
33 180012053     0.00   0.00 0.00  
34 180013688     0.00   0.00 0.00  
35 180029789     0.00   0.00 0.00  
36 180033921     0.00 1 3.23 0.00  
37 180074598     0.00   0.00 0.00  
38 180111515     0.00   0.00 0.00  
39 180147358     0.00   0.00 0.00  

(*) Última atualização: [2019-03-19 Ter 10:33]

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

Email: contato@flaviomoura.mat.br

Created: 2019-03-19 Ter 11:12

Validate