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

Abstract

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.

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.