Navegando por Autor "Silveira, Ariel Agne da"

Filtrar resultados informando as primeiras letras
Agora exibindo 1 - 1 de 1
  • Nenhuma Miniatura Disponível
    Item
    Uma formalização da lógica modal usando o assistente de provas Coq.
    (2023) Silveira, Ariel Agne da; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Vasconcellos, Cristiano Damiani; Reis, Leonardo Vieira dos Santos
    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 nesta tarefa 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 mo- delo. 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.