On fairness in distributed automated deduction

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.