We present a model of parallel search in theorem proving for forward-reasoning strategies, with contraction and distributed search. We extend to parallel search the bounded-search-spaces approach to the measurement of infinite search spaces, capturing both the advantages of parallelization, e.g., the subdivision of work, and its disadvantages, e.g., the cost of communication, in terms of search space. These tools are applied to compare the search space of a distributed-search contraction-based strategy with that of the corresponding sequential strategy.
Analysis of distributed-search contraction-based strategies
BONACINA, Maria Paola
1998-01-01
Abstract
We present a model of parallel search in theorem proving for forward-reasoning strategies, with contraction and distributed search. We extend to parallel search the bounded-search-spaces approach to the measurement of infinite search spaces, capturing both the advantages of parallelization, e.g., the subdivision of work, and its disadvantages, e.g., the cost of communication, in terms of search space. These tools are applied to compare the search space of a distributed-search contraction-based strategy with that of the corresponding sequential strategy.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
JELIA1998parasearch.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
188.87 kB
Formato
Adobe PDF
|
188.87 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.