Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Nalon, Cláudia | - |
Autor(es): dc.creator | Vieira, Thiago Coelho | - |
Data de aceite: dc.date.accessioned | 2024-07-22T12:18:26Z | - |
Data de disponibilização: dc.date.available | 2024-07-22T12:18:26Z | - |
Data de envio: dc.date.issued | 2015-04-20 | - |
Data de envio: dc.date.issued | 2015-04-20 | - |
Data de envio: dc.date.issued | 2015-04-20 | - |
Data de envio: dc.date.issued | 2015-01-07 | - |
Fonte completa do material: dc.identifier | http://dx.doi.org/10.26512/2015.01.D.17951 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/800818 | - |
Descrição: dc.description | Dissertaçã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.description | Diversos 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.description | Logics 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.format | application/pdf | - |
Direitos: dc.rights | Acesso Aberto | - |
Direitos: dc.rights | A 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.subject | Provadores de teoremas | - |
Palavras-chave: dc.subject | Tableaux | - |
Palavras-chave: dc.subject | Verificação formal | - |
Palavras-chave: dc.subject | Lógicas epistêmicas | - |
Palavras-chave: dc.subject | Lógica de crença | - |
Palavras-chave: dc.subject | Lógicas temporais | - |
Palavras-chave: dc.subject | Lógica modal | - |
Título: dc.title | Um provador de teoremas baseado em tableaux para verificação de propriedades temporais de conhecimento ou crença | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: