Realiza-se mais uma sessão do Math Seminar CIDMA/UAlg , que terá como orador Simão Melo de Sousa , da Universidade do Algarve.
Este seminário aborda os fundamentos da verificação formal e do raciocínio automatizado, explorando a relação entre lógica matemática, teoria das demonstrações e informática.
Serão apresentados conceitos como a teoria dos tipos, a correspondência de Curry–Howard, que estabelece uma ligação entre proposições e tipos, e entre demonstrações e programas, bem como métodos de verificação formal de programas.
A sessão incluirá exemplos de ferramentas como Rocq (anteriormente Coq) e Why3, utilizadas na verificação de software e na formalização de resultados matemáticos.
Serão ainda discutidos, caso o tempo o permita, os desafios e as oportunidades associados à utilização da inteligência artificial na descoberta e construção de demonstrações matemáticas, bem como o papel da verificação formal na garantia da sua correção.
Fonte: Centro de Estudos em Património Paisagem e Construção. Horário, local exato e preço na página oficial.
