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 thwartmonotonicity, 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.