Uma formalização da lógica modal usando o assistente de provas Coq.

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorRibeiro, Rodrigo Geraldo-
Autor(es): dc.contributorRoggia, Karina Girardi-
Autor(es): dc.contributorRibeiro, Rodrigo Geraldo-
Autor(es): dc.contributorRoggia, Karina Girardi-
Autor(es): dc.contributorVasconcellos, Cristiano Damiani-
Autor(es): dc.contributorReis, Leonardo Vieira dos Santos-
Autor(es): dc.creatorSilveira, Ariel Agne da-
Data de aceite: dc.date.accessioned2025-08-21T15:56:13Z-
Data de disponibilização: dc.date.available2025-08-21T15:56:13Z-
Data de envio: dc.date.issued2023-11-09-
Data de envio: dc.date.issued2023-11-09-
Data de envio: dc.date.issued2022-
Fonte completa do material: dc.identifierhttp://www.repositorio.ufop.br/jspui/handle/123456789/17720-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/1027940-
Descrição: dc.descriptionPrograma 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.-
Descrição: dc.descriptionA 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.-
Descrição: dc.descriptionThe modelling of certain types of computational systems with classical logic includes limiting factors. In this context, the presentation of other logical systems, such as modal logic, and the construction of a library for the proof assistant Coq intents to help in this work and facilitate usage on the verification of systems’ properties. The semantics of modal logic is represented by the semantics of possible worlds, where there is an accessibility relationship that connects the worlds of a model. Different restrictions imposed on the accessibility relation build modal logic systems that help representation of properties on a wide array of research areas. The libary development aims to held the formalization of properties in softwares and prove them on Coq.-
Formato: dc.formatapplication/pdf-
Idioma: dc.languagept_BR-
Direitos: dc.rightsaberto-
Direitos: dc.rightshttp://creativecommons.org/licenses/by-sa/3.0/us/-
Direitos: dc.rightsAutorizaçã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.-
Palavras-chave: dc.subjectLógica modal-
Palavras-chave: dc.subjectCorreção-
Palavras-chave: dc.subjectCompletude-
Palavras-chave: dc.subjectAssistente de provas-
Título: dc.titleUma formalização da lógica modal usando o assistente de provas Coq.-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional - UFOP

Não existem arquivos associados a este item.