| Abstract [eng] |
Using genetic algorithms, the study aims to find the best possible search strategies for the automatic theorem proving system "E". Individuals of population are coded as search strategies, and they are evaluated using a base of TPTP formulas (problems). Crossing of individuals is performed by transferring clause evaluation functions from parents to children, and mutation is performed by randomly changing weight functions or their parameters in an individual. The experiments revealed that the strategy obtained by the genetic algorithm is better than the automatic strategy of the system "E". A better individual is obtained by performing evolutions with 50, 100 and 200 individuals up to 200 generations. It was also observed that the higher number of weight functions in the strategy increases the number of solved problems. Experiments have shown that the best results are achieved when four or more weight functions are combined in the strategy. |
