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.
On the modelling of search in theorem proving - Towards a theory of strategy analysis
BONACINA, Maria Paola
;
1998-01-01
Abstract
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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
IC1998search.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
282.38 kB
Formato
Adobe PDF
|
282.38 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
