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.