Prof. Marcus Ramos - Provadores de Teoremas e suas Aplicações

01 - 13/07/2018 - Motivação e visão geral (slides).
02 - 20/07/2018 - Exemplo completo (slides e script).
03 - 27/07/2018 - Introdução (preface).
04 - 03/08/2018 - Programação funcional em Coq (functional programming in Coq) - parte 1, programação funcional em Coq. INDUCTIVE, DEFINITION, FIXPOINT, MATCH.
05 - 10/08/2018 - Programação funcional em Coq (functional programming in Coq) - parte 2, programação funcional em Coq, provas por simplificação e reescrita. INTROS, SIMPL, REFLEXIVITY, REWRITE.
06 - 17/08/2018 - Programação funcional em Coq (functional programming in Coq) - parte 3, programação funcional em Coq, provas por análise de casos. DESTRUCT. Exemplos de lógica com Prop (script). SPLIT, LEFT, RIGHT, APPLY, EXACT, TRIVIAL, ABSURD, CONTRADICTION, SPECIALIZE, ASSERT, EXISTS.
07 - 22/08/2018 - Discussão sobre o exercício de representação binária para números naturais. Continuidade dos exemplos de lógica com Prop. Lógica Clássica x Lógica Construtiva.
08 - 31/08/2018 - Provas por indução (proof by induction) - parte 1. INDUCTION.
09 - 14/09/2018 - Provas por indução (proof by induction) - parte 2. Continuidade dos exercícios.
10 - 21/09/2018 - Provas por indução (proof by induction) - parte 3. Continuidade dos exercícios (números binários e naturais, funções de conversão e provas de corretude, slides).
11 - 05/10/2018 - Exemplos com números pares e ímpares (script).
12 - 07/11/2018 - Exemplos do livro FOCS (script).
13 - 23/11/2018 - Dedução Natural e Panda (slides, script e pdf).
14 - 30/11/2018 - Cálculo Lambda Não-Tipado. Linguagem lambda e definições (slides).
15 - 07/12/2018 - Cálculo Lambda Não-Tipado. Substituições, reduções-beta, formas normais, numerais de Church (slides).
16 - 14/12/2018 - Booleanos de Church. Igualdade-beta. Introdução ao Cálculo Lambda Tipado. (slides).
17 - 21/12/2018 - Cálculo Lambda Tipado (capítulo 2 do livro de Nederpelt & Geuvers).

2019

18 - 25/01/2019 - Pares e listas em Coq (working with structured data) - parte 1 (Definições e exemplos).
19 - 01/02/2019 - Pares e listas em Coq (working with structured data) - parte 2. Continuidade dos exercícios (DEFINITIONS and FIXPOINTS).
20 - 08/02/2019 - Pares e listas em Coq (working with structured data) - parte 3. Continuidade dos exercícios (LEMMAS and THEOREMS).
21 - 15/02/2019 - Pares e listas em Coq (working with structured data) - parte 4. Continuidade dos exercícios (OPTION and MAP).
22 - 22/02/2019 - Revisão de Cálculo Lambda Tipado (slides) - parte 1. Motivação e definições.
23 - 27/02/2019 - Revisão de Cálculo Lambda Tipado (slides) - parte 2. Problemas e propriedades.
24 - 22/03/2019 - Revisão de Cálculo Lambda Tipado (slides) - parte 3. Propriedades e exercícios.
25 - 26/04/2019 - Polimorfismo e funções de alta ordem (polymorphism and higher-order functions) - parte 1.
26 - 03/05/2019 - Polimorfismo e funções de alta ordem (polymorphism and higher-order functions) - parte 2.
27 - 10/05/2019 - Revisão do conteúdo dos dois encontros anteriores.
28 - 17/05/2019 - Polimorfismo e funções de alta ordem (polymorphism and higher-order functions) - parte 3.
29 - 31/05/2019 - Polimorfismo e funções de alta ordem (polymorphism and higher-order functions) - parte 4.
30 - 14/06/2019 - Táticas (more basic tactics) - parte 1.
31 - 28/06/2019 - Táticas (more basic tactics) - parte 2.
32 - 05/07/2019 - Táticas (more basic tactics) - parte 3.
33 - 02/08/2019 - Apresentação do projeto de formalização da teoria das linguagens livres de contexto. Discussão de quatro possibilidades de projeto: (i) Questões decidíveis para as linguagens livres de contexto (pertencimento, vacuidade e infinitude); (ii) Redução do PL para as LLC para o PL para as LR; (iii) Equivalência entre GLDs e GLEs; (iv) Redução MPCP -> PCP.
34 - 09/08/2019 - Discussão dos projetos de formalização (i) e (iii) e revisão da teoria; detalhamento da formalização da teoria das linguagens livres de contexto em Coq, apresentação e análise das definições básicas (terminais, não-terminais, formas sentenciais, sentenças e gramáticas).
35 - 30708/2019 - Definição indutiva para derivações em gramáticas livres de contexto. Exemplos e exercícios.
36 - 13/09/2019 - Discussão dos problemas atuais envolvendo duas formalizações: questões decidíveis das linguagens livres de contexto e equivalência entre gramáticas lineares à direita e à esquerda.
37 - 27/09/2019 - Gramáticas lineares à direita e à esquerda (slides).
38 - 04/10/2019 - Discussão sobre a formalização do algoritmo de conversão de GLDs em GLDs que geram a linguagem reversa e sua correção.
39 - 11/10/2019 - Prova (parcial) do lema "rl_to_rl_reverse_derives_2" do arquivo "regular.v".
40 - 25/10/2019 - Planejamento do mini-curso que será ministrado durante o ERMAC na UNIVASF (teoria e prática). Ajustes com a coordenação do evento.
41 - 08/11/2019 - Definição dos exemplos e exercícios que serão usados no ERMAC.
42 - 06/12/2019 - Retomada dos esforços para a prova do lema "rl_to_rl_reverse_derives_2" do arquivo "regular.v". Definição de uma estratégia para uma prova informal e formalização de uma forma normal para GLDs (com una única regra vazia e todas as demais no formato X -> aY ou X -> Y).
43 - 20/12/2019 - Leitura da transcrição das conclusões do encontro anterior e revisão do conteúdo das notas (slides).

2020

44 - 31/01/2020 - Retomada das discussões sobre a conversão de GLDs para GLDs que geram a linguagem reversa. Pequena reformulação do algoritmo da forma normal para GLDs e prova informal. Planejamento dos próximos encontros. (slides).