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.

On fairness in distributed automated deduction

BONACINA, Maria Paola;
1993

Abstract

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.
9783540565031
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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: http://hdl.handle.net/11562/16056
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact