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

Metodologia: 

Descrição do projeto:

Acreditamos ser de extrema importância fornecer a nossos alunos uma formação conectada com os grandes desafios da Ciência da Computação do terceiro milênio, que incluem a capacidade de produzir software verificado formalmente e livre de erros. Desenvolvimento dessas habilidades incrementam a versatilidade do profissional de Ciência da Computação para lidar com precisão tanto com a sua área de formação quanto com áreas nas quais esta ciência é aplicada (engenharia, ciências medicas, ciências biológica, administração, ciências exatas). Promover o desenvolvimento dessa versatilidade nos estudantes da área exige uma abordagem didática que, além das atividades práticas, inclua também um considerável esforço para garantir o estudo interessado de considerável quantidade de material teórico, como é o caso dos cursos de Lógica Computacional e Projeto e Análise de Algoritmos considerados nessa proposta.

Objetivo geral: 

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