Ribeiro, Rodrigo GeraldoRoggia, Karina GirardiSilveira, Ariel Agne da2023-11-102023-11-102023SILVEIRA, Ariel Agne da. Uma formalização da lógica modal usando o assistente de provas Coq. 2023. 57 f. Dissertação (Mestrado em Ciência da Computação) - Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto, Ouro Preto, 2023.http://www.repositorio.ufop.br/jspui/handle/123456789/17720Programa de Pós-Graduação em Ciência da Computação. Departamento de Ciência da Computação, Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto.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.pt-BRabertohttp://creativecommons.org/licenses/by-sa/3.0/us/Lógica modalCorreçãoCompletudeAssistente de provasDissertacaoAutorização concedida ao Repositório Institucional da UFOP pelo(a) autor(a) em 23/10/2023 com as seguintes condições: disponível sob Licença Creative Commons 4.0 que permite copiar, distribuir e transmitir o trabalho, desde que sejam citados o autor e o licenciante.