Abstract
One problem that chain format linear deduction systems can suffer from is the necessity of repeating subdeductions when unifiable literals appear in (possibly distinct) centre chains of a deduction. Four mechanisms for avoiding the repetition are: factoring, lemmas, C-literals, and caching. These mechanisms are examined, and it is concluded that lemmas and C-literals are the mechanisms of choice for this task. A correspondance between the lemma and C-literal mechanisms is described, leading to the introduction of two new repetition avoidance mechanisms. Lemmas, C-literals, and the two new mechanisms have been performance tested. It is concluded that the absolute benefit of using any repetition avoidance mechanism is not large (in the test suite used), but that the C-literal and one of the new mechanisms do improve the performance of the host deduction system.