On subsumption in distributed derivations

In this paper we study the subsumption inference rule in the context of distributed deduction. It is well known that the unrestricted application of subsumption may destroy the fairness and thus the completeness of a deduction strategy. Solutions to this problem in sequential theorem proving are known. We observe that in distributed automated deduction, subsumption may also thwart monotonicity, a dual property of soundness, in addition to completeness. Not only do the solutions for the sequential case not apply, even proper subsumption may destroy monotonicity in the distributed case. We present these problems and propose a general solution that treats subsumption as a composition of a replacement inference rule, replacement subsumption, and a deletion inference rule, variant subsumption. (Proper subsumption, in this case, becomes a derived inference rule.) We define a new distributed subsumption inference rule, which has all the desirable properties: it allows subsumption, including subsumption of variants, in a distributed derivation, while preserving fairness and monotonicity. It also works in both sequential and distributed environments. We conclude the paper with some discussion of the different behavior of subsumption in different architectures.