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

We present a model for representing search in theorem proving. This model captures the notion of contraction, 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.

• Type: Journal
• Year: 1998
• Where: IANDC
• Authors: Maria Paola Bonacina, Jieh Hsiang
• Keywords: Different Contraction Power, IANDC 1998, Model, Respective Search Spaces