Utilize este link para identificar ou citar este item:
https://bdm.unb.br/handle/10483/31259
| Título: | Algoritmos de seleção de cláusulas em provas por resolução para lógicas modais |
| Autor(es): | Leite, José Marcos da Silva |
| Orientador(es): | Nalon, Cláudia |
| Assunto: | Lógica modal
Provador de teoremas interativo
Seleção de cláusula |
| Data de apresentação: | 5-Nov-2021 |
| Data de publicação: | 28-Jun-2022 |
| Referência: | 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. |
| Resumo: | 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. |
| Abstract: | 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. |
| 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, 2021. |
| Licença: | 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. |
| Aparece na Coleção: | Ciência da Computação
|
Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.
