This paper presents a taxonomy of parallel theorem-proving methods based on the control of search (e.g., master-slaves versus peer processes), the granularity of parallelism (e.g., fine, medium and coarse grain) and the nature of the method (e.g., ordering-based versus subgoal-reduction). We analyze how the different approaches to parallelization affect the control of search: while fine and medium-grain methods, as well as master-slaves methods, generally do not modify the sequential search plan, parallel-search methods may combine sequential search plans (multi-search) or extend the search plan with the capability of subdividing the search space (distributed search). Precisely because the search plan is modified, the latter methods may produce radically different searches than their sequential base, as exemplified by the first distributed proof of the Robbins theorem generated by the Modified Clause-Diffusion prover Peers-mcd. An overview of the state of the field and directions for future research conclude the paper.

A taxonomy of parallel strategies for deduction

BONACINA, Maria Paola
2000-01-01

Abstract

This paper presents a taxonomy of parallel theorem-proving methods based on the control of search (e.g., master-slaves versus peer processes), the granularity of parallelism (e.g., fine, medium and coarse grain) and the nature of the method (e.g., ordering-based versus subgoal-reduction). We analyze how the different approaches to parallelization affect the control of search: while fine and medium-grain methods, as well as master-slaves methods, generally do not modify the sequential search plan, parallel-search methods may combine sequential search plans (multi-search) or extend the search plan with the capability of subdividing the search space (distributed search). Precisely because the search plan is modified, the latter methods may produce radically different searches than their sequential base, as exemplified by the first distributed proof of the Robbins theorem generated by the Modified Clause-Diffusion prover Peers-mcd. An overview of the state of the field and directions for future research conclude the paper.
2000
Automated theorem proving; ordering-based strategies; resolution; subgoal-reduction strategies; model elimination; parallel rewriting; parallel deduction; parallel search; distributed search
File in questo prodotto:
File Dimensione Formato  
AMAI2000paratax.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 307.43 kB
Formato Adobe PDF
307.43 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/16030
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 15
social impact