Repositório Digital

A- A A+

Continuação do desenvolvimento de um provador de teoremas para a lógica clássica de primera ordem e criação de um raciocinador com o método analítico de Tableau para uma lógica de descrição

.

Continuação do desenvolvimento de um provador de teoremas para a lógica clássica de primera ordem e criação de um raciocinador com o método analítico de Tableau para uma lógica de descrição

Mostrar registro completo

Estatísticas

Título Continuação do desenvolvimento de um provador de teoremas para a lógica clássica de primera ordem e criação de um raciocinador com o método analítico de Tableau para uma lógica de descrição
Outro título Further development of a theorem prover for classical firstorder logic and design of an analytic tableau reasoner for a description logic
Autor Cravo, Diogo Raphael
Orientador Moreira, Alvaro Freitas
Data 2015
Nível Graduação
Instituição Universidade Federal do Rio Grande do Sul. Instituto de Informática. Curso de Ciência da Computação: Ênfase em Engenharia da Computação: Bacharelado.
Assunto Lógica
Logica : Descricao
[en] Classical logic
[en] Description logics
[en] FOL
[en] Tableau
[en] Theorem prover
Resumo Durante o Semestre de Inverno de 2013 a 2014 aconteceu o módulo “Projekt: Symbolische Künstliche Intelligenz”. Neste módulo os estudantes criaram um provador de teoremas para a lógica clássica de primeira ordem. O provador criado na época conseguia através da aplicação de seis diferentes métodos checar a insatisfatibilidade ou validade de fórmulas bem como a consistência de bases de conhecimento. Este Trabalho de Graduação apresenta a continuação do desenvolvimento desse provador de teoremas. Entre as novas funcionalidades do provador estão várias estratégias do método de Tableau, como o Tableau analítico de Smullyan e o Tableau com variáveis livres de Fitting, assim como representações gráficas das provas. Além disto o Software também consegue resolver o problema da subsunção da lógica de descrição ALC. O Software implementado é fácil de usar e vários módulos podem ser reutilizados. Finalmente todas as estratégias utilizadas neste trabalho foram avaliadas por 68 testes, através do que a ineficiência da implementação foi constatada. Melhorias são sugeridas no fim.
Abstract During the Winter Semester from 2013 to 2014 the Project “Projekt: Symbolische Künstliche Intelligenz” took place. During that project the students have created a theorem prover for the firstorder logic. The prover created in this time could check the unsatisfiability or validity of formulas as well as the consistency of knowledge bases by applying six different approaches. This Bachelor’s Thesis presents the further development of that theorem prover. The new prover offers new functionalities, such as the analytical Smullyan Tableau and the free Variable Tableau by Fitting, as well as graphical representations of proofs. Furthermore the Software can solve the subsumption problem of the ALC Description Logic. The implemented Software is easy to use and many of its modules are reusable. Finally all approaches implemented in this work were evaluated by the application of 68 Tests, which revealed the bad performance of the implementation. Improvements are suggested in the end.
Tipo Trabalho de conclusão de graduação
URI http://hdl.handle.net/10183/126062
Arquivos Descrição Formato
000972312.pdf (1.878Mb) Texto completo Adobe PDF Visualizar/abrir

Este item está licenciado na Creative Commons License

Este item aparece na(s) seguinte(s) coleção(ões)


Mostrar registro completo

Percorrer



  • O autor é titular dos direitos autorais dos documentos disponíveis neste repositório e é vedada, nos termos da lei, a comercialização de qualquer espécie sem sua autorização prévia.
    Projeto gráfico elaborado pelo Caixola - Clube de Criação Fabico/UFRGS Powered by DSpace software, Version 1.8.1.