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

Página do item simplificado
dc.contributor.advisorRibeiro, Rodrigo Geraldopt_BR
dc.contributor.advisorRoggia, Karina Girardipt_BR
dc.contributor.authorSilveira, Ariel Agne da
dc.contributor.refereeRibeiro, Rodrigo Geraldopt_BR
dc.contributor.refereeRoggia, Karina Girardipt_BR
dc.contributor.refereeVasconcellos, Cristiano Damianipt_BR
dc.contributor.refereeReis, Leonardo Vieira dos Santospt_BR
dc.date.accessioned2023-11-10T17:50:44Z
dc.date.available2023-11-10T17:50:44Z
dc.date.issued2023pt_BR
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.pt_BR
dc.description.abstractA 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_BR
dc.description.abstractenThe 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.pt_BR
dc.identifier.citationSILVEIRA, 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.pt_BR
dc.identifier.urihttp://www.repositorio.ufop.br/jspui/handle/123456789/17720
dc.language.isopt_BRpt_BR
dc.rightsabertopt_BR
dc.rights.licenseAutorizaçã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.pt_BR
dc.rights.urihttp://creativecommons.org/licenses/by-sa/3.0/us/*
dc.subjectLógica modalpt_BR
dc.subjectCorreçãopt_BR
dc.subjectCompletudept_BR
dc.subjectAssistente de provaspt_BR
dc.titleUma formalização da lógica modal usando o assistente de provas Coq.pt_BR
dc.typeDissertacaopt_BR

Arquivos

Pacote original

Agora exibindo 1 - 1 de 1
Nenhuma Miniatura Disponível
Nome:
DISSERTAÇÃO_FormalizaçãoLógicaModal.pdf
Tamanho:
618.34 KB
Formato:
Adobe Portable Document Format
Descrição:
Baixar

Licença do pacote

Agora exibindo 1 - 1 de 1
Nenhuma Miniatura Disponível
Nome:
license.txt
Tamanho:
1.71 KB
Formato:
Item-specific license agreed upon to submission
Descrição:
Baixar

Coleções

PPGCC - Mestrado (Dissertações)