Coordenador(a) do projeto: Prof. Flávio Leonardo Cavalcanti de Moura

Metodologia(s): 

Descrição do projeto:

Esse projeto pretende envolver professoras e estudantes de duas universidades, UnB e Unicamp, embora o braço no presente edital se dirija especialmente aos estudantes de graduação do DAN e da UnB.

Objetivo(s) geral(is): 

O presente projeto tem como foco a preparação de material didático para efetiva capacitação de estudantes de Ciência da Computação na construção de provas de correção de algoritmos utilizando as técnicas dedutivas da lógica de primeira ordem. Esse material será aplicado nas turmas das disciplinas 117366 – Lógica Computacional 1 e 117536 – Projeto e Análise de Algoritmos, disciplinas com uma alta taxa histórica de desistência. O material apresentará desafios simples que motivarão os estudantes sobre a relevância e importância das tecnologias dedutivas lógicas para aplicações verificação de correção de algoritmos. Os alunos deverão desenvolver suas formalizações matemáticas com o auxílio de um assistente de provas.

Produtos: 

Referência: Edital CEADn. 01/2019