Um provador de teoremas baseado em tableaux para verificação de propriedades temporais de conhecimento ou crença

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorNalon, Cláudia-
Autor(es): dc.creatorVieira, Thiago Coelho-
Data de aceite: dc.date.accessioned2024-10-23T15:51:54Z-
Data de disponibilização: dc.date.available2024-10-23T15:51:54Z-
Data de envio: dc.date.issued2015-04-20-
Data de envio: dc.date.issued2015-04-20-
Data de envio: dc.date.issued2015-04-20-
Data de envio: dc.date.issued2015-01-07-
Fonte completa do material: dc.identifierhttp://dx.doi.org/10.26512/2015.01.D.17951-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/894001-
Descrição: dc.descriptionDissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, Mestrado em Informática, 2015.-
Descrição: dc.descriptionDiversos tipos de lógicas são usadas como linguagens para descrever sistemas complexos e suas propriedades com a finalidade de serem verificadas formalmente. Provadores de teoremas baseados em tableaux são ferramentas computacionais capazes de realizar esta tarefa de verificação. Em (WDF98) é proposto um método de prova baseado em tableaux para duas lógicas epistêmico-temporais, KL(n) e BL(n). Neste trabalho implementamos o método de prova baseado em tableaux descrito em (WDF98) e apresentamos um algoritmo para verificação de propriedades epistêmicas e temporais sobre a estrutura do tableau construída por este método.-
Descrição: dc.descriptionLogics are used as languages to describe complex systems and their properties in order to be formally verified. Tableaux-based theorem-provers are computational tools which can be used to perform this verification task. (WDF98) propose a proof method based on tableaux for both the epistemic-temporal logics KL(n) and BL(n) . In this work we implement the tableaux-based proof method described in (WDF98) and present an algorithm for verification of epistemic-temporal properties over the structure of the tableau built by this method.-
Formato: dc.formatapplication/pdf-
Direitos: dc.rightsAcesso Aberto-
Direitos: dc.rightsA concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.-
Palavras-chave: dc.subjectProvadores de teoremas-
Palavras-chave: dc.subjectTableaux-
Palavras-chave: dc.subjectVerificação formal-
Palavras-chave: dc.subjectLógicas epistêmicas-
Palavras-chave: dc.subjectLógica de crença-
Palavras-chave: dc.subjectLógicas temporais-
Palavras-chave: dc.subjectLógica modal-
Título: dc.titleUm provador de teoremas baseado em tableaux para verificação de propriedades temporais de conhecimento ou crença-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional – UNB

Não existem arquivos associados a este item.