| Summary: | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas,
Departamento de Ciência da Computação,
Mestrado em Informática, 2015. === Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2015-03-31T15:40:32Z
No. of bitstreams: 1
2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) === Approved for entry into archive by Ruthléa Nascimento(ruthleanascimento@bce.unb.br) on 2015-04-20T19:01:54Z (GMT) No. of bitstreams: 1
2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) === Made available in DSpace on 2015-04-20T19:01:54Z (GMT). No. of bitstreams: 1
2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) === 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. === 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.
|
|---|
