CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThis 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.
| Titolo: | A taxonomy of parallel strategies for deduction |
| Autori: | |
| Data di pubblicazione: | 2000 |
| Rivista: | |
| Handle: | http://hdl.handle.net/11562/16030 |
| Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
http://hdl.handle.net/11562/16030
Copyright © 2021