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.
EnglishWe present a new approach to distributed automated deduction and in this context we propose solutions to the problem of distributed uniform fairness. Given a sequential theorem proving strategy and an input problem, our methodology partitions the clauses and the expansion inferences among the nodes of the distributed environment, establishing a derivation at each node. A distributed derivation is defined as a family of concurrent, asynchronous derivations, communicating clauses through message-passing. As soon as one of the local derivations finds a proof, the distributed derivation halts successfully. Uniform fairness requires that all clauses which can be derived from persistent, non-redundant parents are generated eventually. In the distributed case, it comprises fairness of message-passing, which is necessary to make sure that any two persistent, non-redundant clauses, residents at different nodes, meet eventually. We reduce the abstract definition of uniform fairness for general derivations to a more concrete specification of uniform fairness for distributed derivations, by proving that the latter implies the former. Then, we describe mechanisms which can be embedded in a strategy to satisfy these conditions. We conclude the paper with some discussion on the relevance of our results to other applications of distributed databases.
| Titolo: | On fairness in distributed automated deduction |
| Autori: | |
| Data di pubblicazione: | 1993 |
| Serie: | |
| Handle: | http://hdl.handle.net/11562/16056 |
| ISBN: | 9783540565031 |
| Appare nelle tipologie: | 02.01 Contributo in volume (Capitolo o Saggio) |
File in questo prodotto:
Copyright © 2020