Otimização de métodos de prova em tablôs KE através da aplicação de uma heurística baseada em algoritmos genéticos

Abstract

This work presents an approach for optimizing the proof methods in the KE system based on Genetic Algorithms. The focus of this work is on the PB (Principle of bivalence) rule, which bifurcates the tableau and increases the proof cost. The selection of PB candidates is based on concepts expressed in Natural Selection Genetic Algorithm approach, so that formulas that enable increased variation in the knowledge base are considered more suitable than others. The selection of the most suitable formula is compared with the conventional proof method for KE system in a computing environment via an automated theorem prover. The increased variability of the knowledge base provided by the pre-selection of PB candidates demonstrates an optimization of proof methods in comparison with the conventional methodology. This is due to the fact that the greater the number of different premises it is more likely that an inconsistency is generated in the knowledge base, consequently, the tableau will be closed.