Future directions of automated deduction: Strategy analysis for theorem proving
Maria Paola Bonacina · 1996
ces. The main reason for the absence of "strategy analysis" is the lack of formal tools to analyze the complexity of problems involving search in an infinite search space. There are several obstacles in analyzing the complexity of search in an infinite space, including the following: ffl The methodology of traditional complexity analysis is not suitable, because it is concerned mainly with the asymptotic analysis of finite objects, with time and space the two dominating measures. Given that the search space is infinite, it is no longer meaningful to discuss about average case analysis, much less worst case. Supported in part by the National Science Foundation with grant CCR-94-08667. ffl In a finite problem the time and space complexities can usually be treated as functions of a measure of the input. But for first-order logic, for instance, the difficulty of finding a proof is not relate