| Campo Dublin Core | Valor | Língua |
|---|
| dc.contributor.advisor | Nalon, Cláudia | - |
| dc.contributor.author | Menezes, André Belle | - |
| dc.identifier.citation | MENEZES, André Belle. Métodos polinomiais para simplificação de fórmulas modais. 2016. x, 41 f., il. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação)—Universidade de Brasília, Brasília, 2016. | pt_BR |
| dc.description | Trabalho de Conclusão de Curso (graduação)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2016. | pt_BR |
| dc.description.abstract | A simplificação de fórmulas lógicas busca melhorar a eficiência do tratamento destas. Este projeto desenvolve um algoritmo baseado na eliminação de literal puro e propagação de constante para realizar simplificação. O trabalho é realizado em cima do provador KSP que já implementa os métodos de simplificação citados, porém acreditamos que esse novo algoritmo desenvolvido trará maior desempenho na execução. Como melhorias foram propostas uma lista de localização para as proposições das fórmulas e a realização de eliminação de literal puro enquanto isso for possível. A implementação é explicada detalhadamente neste trabalho. As comparações realizadas entre as versões dos provadores mostra que a nova versão é melhor para algumas fórmulas e o KSP para outras. Apesar disso, a nova implementação pode produzir fórmulas mais simplificadas e sua manipulação das estruturas de dados é mais eficiente, porém os tempos de execução não foram afetados de maneira substancial. | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject.keyword | Lógica modal | pt_BR |
| dc.subject.keyword | Algoritmos | pt_BR |
| dc.title | Métodos polinomiais para simplificação de fórmulas modais | pt_BR |
| dc.type | Trabalho de Conclusão de Curso - Graduação - Bacharelado | pt_BR |
| dc.date.accessioned | 2017-04-06T17:08:29Z | - |
| dc.date.available | 2017-04-06T17:08:29Z | - |
| dc.date.submitted | 2016 | - |
| dc.identifier.uri | http://bdm.unb.br/handle/10483/16546 | - |
| dc.language.iso | Português | pt_BR |
| dc.description.abstract1 | Simplification of logical formulae is a preprocessing procedure which seeks to reduce the size of the input formula in order to improve the overall efficiency of theorem provers. This project implements two procedures for simplification: one for pure literal elimination and other for constant propagation. The work is based on an existing prover, KSP, which already implements the mentioned simplification methods. However, our hypothesis was that our implementation would improve performance by changing the underlying data
structures. One of the implementation improvements proposed was a localization list for the propositions of the formulae. Also, pure literal elimination is executed until a fixed-point is reached. We explain the implementation in detail. Comparison between the provers versions show that there is no time difference pattern, but the new implementation usually produces results in less time. The new implementation produces better formulae in some cases and makes good use of data structures, but execution times have not been
substantially affected. | pt_BR |
| Aparece na Coleção: | Ciência da Computação
|
