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.
1998
9783540651413
distributed-search; contraction-based strategies
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16046
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact