We investigate the usage of so-called self-modifying theorem provers. We point out the problems arising from the inflexibility of existing approaches to heuristically control the search of automated deduction systems, and we propose the application of systems adapting themselves to the actual proof problem by periodically judging their work done on the problem. We study the modification of search states as well as the adaptation of the search heuristic based on the classification of proof results. Moreover, we report on experimental results obtained in the area of condensed detachment.
logic calculi, condensed detachment, self-modification, classification, deactivation