On the Modelling of Search in Theorem Proving— Towards a Theory of Strategy Analysis

AbstractWe present a model for representing search in theorem proving. This model captures the notion ofcontraction, which has been central in some of the recent developments in theorem proving. We outline an approach to measuring the complexity of search which can be applied to analyze and evaluate the behaviour of theorem-proving strategies. Using our framework, we compare contraction-based strategies of different contraction power and show how they affect the evolution of the respective search spaces during the derivation