Show simple item record

dc.contributor.advisorMoreira, Alvaro Freitaspt_BR
dc.contributor.authorCravo, Diogo Raphaelpt_BR
dc.date.accessioned2015-08-29T02:40:09Zpt_BR
dc.date.issued2015pt_BR
dc.identifier.urihttp://hdl.handle.net/10183/126062pt_BR
dc.description.abstractDurante 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.pt_BR
dc.description.abstractDuring 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.en
dc.format.mimetypeapplication/pdf
dc.language.isoporpt_BR
dc.rightsOpen Accessen
dc.subjectTableauen
dc.subjectLógicapt_BR
dc.subjectLogica : Descricaopt_BR
dc.subjectTheorem proveren
dc.subjectClassical logicen
dc.subjectDescription logicsen
dc.subjectFOLen
dc.titleContinuaçã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çãopt_BR
dc.title.alternativeFurther development of a theorem prover for classical firstorder logic and design of an analytic tableau reasoner for a description logic en
dc.typeTrabalho de conclusão de graduaçãopt_BR
dc.identifier.nrb000972312pt_BR
dc.degree.grantorUniversidade Federal do Rio Grande do Sulpt_BR
dc.degree.departmentInstituto de Informáticapt_BR
dc.degree.localPorto Alegre, BR-RSpt_BR
dc.degree.date2015pt_BR
dc.degree.graduationCiência da Computação: Ênfase em Engenharia da Computação: Bachareladopt_BR
dc.degree.levelgraduaçãopt_BR


Files in this item

Thumbnail
   

This item is licensed under a Creative Commons License

Show simple item record