Resumo

Métodos formais compreendem uma ampla gama de técnicas e ferramentas para raciocínio guiado por computadores e estão sendo adotados como padrão de verificação tanto na academia quanto na indústria. Dentre eles descatacam-se os assistentes de prova, i.e., programas especializados em aplicar os fundamentos formais da matemática para o auxílio e verificação de provas. Estas ferramentas já foram utilizadas com sucesso para checagem de provas não triviais, como por exemplo o Teorema das Quatro Cores. Além disso, assistente de prova vêm ganhando considerável atenção na comunidade matemática. Este contexto torna inegável a necessidade de introduzirmos tais ferramentas para nossos alunos. Sendo assim, neste mini-curso, vamos explorar o uso de assistentes de prova com um exemplo didático clássico: a construção dos números. Focaremos nos números naturais, e de forma construtiva iremos trabalhar em provar suas principais propriedades. Ao final, os alunos terão uma ideia inicial do uso de assistentes de prova e serão capazes de compreender, formalmente, os princípios indutivos possíveis sobre os naturais e compará-los ao que usualmente é utilizado no papel e caneta.

Programação

O mini-curso será dividido em 4 aulas (2h) expositivas e práticas com os alunos desenvolvendo provas no provador. Em cada uma das aulas abordaremos os seguintes tópicos.

1. Introdução aos métodos formais, definição indutiva dos naturais e os axiomas de Peano.
2. Funções recursivas e correspondência de padrões.
3. Predicados indutivos a noção de decidibilidade sobre ℕ.
4. Princípios de ordem.

Públicos Alvo

Interno:

Discentes de graduação com interesse em matemática

Externo:

Toda a comunidade local com interesse em matemática

Membros(as) da Equipe

DEIVID RODRIGUES DO VALE Categoria: DOCENTE Função : COORDENADOR(A)

DANIELE NANTES SOBRINHO Categoria: DOCENTE Função : COORDENADOR ADJUNTO DOCENTE

LUIZA DE OLIVEIRA FELIX Categoria: DISCENTE Função : ALUNO(A) VOLUNTARIO(A)

Lista de Fotos

Não há fotos cadastradas para esta ação