Qualificação de mestrado do discente Ariel Agne, dia 29/09, as 19:00

Qualificação de mestrado do discente Ariel Agne, dia 29/09, as 19:00

Título: Uma formalização da lógica modal usando o assistente de provas Coq
Resumo: A modelagem de determinados tipos de sistemas computacionais com a lógica clássica possui fatores limitantes. Neste contexto, a apresentação de outros sistemas lógicos, como a lógica modal, e a construção de uma biblioteca para o assistente de provas Coq tem o intuito de auxiliar na modelagem e facilitar o uso para a verificação de propriedades de sistemas. A semântica da lógica modal é representada pela semântica dos mundos possíveis, onde existe uma relação de acessibilidade que conecta os mundos de um modelo. Diferentes restrições impostas na relação de acessibilidade constroem sistemas da lógica modal que auxiliam na representação de propriedades nas mais diversas áreas de estudo. O desenvolvimento da biblioteca tem como objetivo sustentar a formalização de propriedades de softwares e prová-los em Coq.
Banca: Prof. Dr. Rafael Alves Bonfim de Queiroz; Profa. Dra. Karina Girardi Roggia

Link para reunião
meet.google.com/umv-yziu-adi