We 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) |