| Campo Dublin Core | Valor | Língua |
|---|
| dc.contributor.advisor | Nalon, Cláudia | - |
| dc.contributor.author | Leite, José Marcos da Silva | - |
| dc.identifier.citation | LEITE, José Marcos da Silva. Algoritmos de seleção de cláusulas em provas por resolução para lógicas modais. 2021. ix, 27 f., il. Trabalho de conclusão de curso (Bacharelado em Ciência da Computação) — Universidade de Brasília, Brasília, 2021. | 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, 2021. | pt_BR |
| dc.description.abstract | Neste trabalho, propomos algumas heurísticas de seleção de cláusulas para provadores de Lógica Modal baseado em resolução e as comparamos a algumas já existentes. A implementação foi feita modificando o provador KSP. Ao adaptar estratégias de lógicas superiores conseguimos pequena melhora que se manteve após expandir a técnica de forma dinâmica. Analisamos ainda uma estratégia para as características específicas do problema, mas não houve melhoria. Um possível trabalho futuro consiste em analisar os motivos de não haver melhora, bem como a seleção do conjunto de candidatos. | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject.keyword | Lógica modal | pt_BR |
| dc.subject.keyword | Provador de teoremas interativo | pt_BR |
| dc.subject.keyword | Seleção de cláusula | pt_BR |
| dc.title | Algoritmos de seleção de cláusulas em provas por resolução para lógicas modais | pt_BR |
| dc.type | Trabalho de Conclusão de Curso - Graduação - Bacharelado | pt_BR |
| dc.date.accessioned | 2022-06-28T22:17:57Z | - |
| dc.date.available | 2022-06-28T22:17:57Z | - |
| dc.date.submitted | 2021-11-05 | - |
| dc.identifier.uri | https://bdm.unb.br/handle/10483/31259 | - |
| dc.language.iso | Português | pt_BR |
| dc.rights.license | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. | pt_BR |
| dc.description.abstract1 | This work proposes new clause selection methods for resolution-based provers and compares them to existing ones. All algorithms were implemented and tested in KSP. First-order methods were adapted to modal logic and there was some improvement that was maintaned after dynamic scheduling. A new method was developed exploiting the particular structure of modal problems but it did not perform well. Future work includes finer analysis of the new method and a closer look into the candidate clause selection for resolution rules GEN1 and GEN3 to see it they can contribute to further performance improvement. | pt_BR |
| Aparece na Coleção: | Ciência da Computação
|
