On subsumption in distributed derivations

The subsumption inference rule in the context of distributed deduction was studied. Unlimited use of subsumption may destroy the completeness of a deduction strategy. In distributed automated deduction, subsumption may also cut-short monotonicity, in addition to completeness. A solution to the problems mentioned may be this new distributed subsumption inference rule which has all the desirable properties. It allowed subsumption, including subsumption of variants, in a distributed derivation, while preserving fairness and monotonicity. It also worked in both sequential and distributed environments.