Strategy analysis

Strategy analysis aims at complementing the experimental evaluation of theorem provers with mathematical models of the behavior of strategies that capture their essential features and establish comparative results. I developed a methodology for strategy analysis which models together search space and search process by means of marked search graphs, and measures search complexity, even in infinite search spaces, by means of bounded search spaces. This also led me to a taxonomy of theorem-proving strategies based on search rather than inferences: A forerunner of this research was a formalization of concepts in theorem proving, including search plan:

Maria Paola Bonacina