| Campo Dublin Core | Valor | Língua |
|---|
| dc.contributor.advisor | Nalon, Cláudia | - |
| dc.contributor.author | Angelos, Daniella Albuquerque dos | - |
| dc.identifier.citation | ANGELOS, Daniella Albuquerque dos. Tableaux clausal para lógica modal. 2016. ix, 40 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 | Este trabalho apresenta a definição de um cálculo tableaux clausal proposto para lógicas modais, além de apresentar uma implementação do mesmo. O objetivo geral é aplicar o método refutacional tableaux utilizando a forma normal construída para resolução clausal na tentativa de gerar o máximo de informações possíveis sobre conjuntos de fórmulas na linguagem modal, sem que seja necessário a especificação de um número elevado de regras de inferência no cálculo, o que tornaria a tarefa de implementar razoavelmente mais difícil. Estas informações extraídas contêm singularidades dos conjuntos de fórmulas que podem auxiliar em decisões relacionadas aos métodos de provas aplicados aos mesmos. As provas de correção para o cálculo são apresentadas. A implementação realizada, apesar de bem sucedida, revelou imperfeições com relação ao desempenho de execução. Esforços direcionados à melhoria de tais imperfeições, bem como uma análise das informações extraídas, são deixados como trabalhos futuros. | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject.keyword | Lógica modal | pt_BR |
| dc.subject.keyword | Tableaux clausal | pt_BR |
| dc.title | Tableaux clausal para lógica modal | pt_BR |
| dc.type | Trabalho de Conclusão de Curso - Graduação - Bacharelado | pt_BR |
| dc.date.accessioned | 2017-08-11T20:07:26Z | - |
| dc.date.available | 2017-08-11T20:07:26Z | - |
| dc.date.submitted | 2016-01-30 | - |
| dc.identifier.uri | http://bdm.unb.br/handle/10483/17860 | - |
| dc.language.iso | Português | pt_BR |
| dc.description.abstract1 | This work presents a clausal tableaux calculus for modal logics and na implementation for it. The main goal is to combine aspects of two different proof methods, the inference rules of a tableaux calculus and the normal form employed in a clausal resolution method. The goal is to generate as much information as possible about sets of formulae in modal logic, without the need to define a large number of inference rules in the calculus, which would make the job of implementing the calculus reasonably harder. The pieces of extracted
information may help to characterise singularities of the set of formulae, which
could then help to make decisions about what proof method to apply to such a set. The implementation is correct, but does not perform well. Efforts in the direction of a more robust implementation and the analysis of the extracted information are left as future work. | pt_BR |
| Aparece na Coleção: | Ciência da Computação
|
