Utilize este link para identificar ou citar este item:
https://bdm.unb.br/handle/10483/16546
| Título: | Métodos polinomiais para simplificação de fórmulas modais |
| Autor(es): | Menezes, André Belle |
| Orientador(es): | Nalon, Cláudia |
| Assunto: | Lógica modal
Algoritmos |
| Data de apresentação: | 2016 |
| Data de publicação: | 6-Abr-2017 |
| Referência: | 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. |
| Resumo: | 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. |
| Abstract: | 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. |
| Informações adicionais: | 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. |
| Aparece na Coleção: | Ciência da Computação
|
Este item está licenciado na Licença Creative Commons
