On free abelian categories for theorem proving

We give a computational approach to theorem proving in homological algebra. This approach is based on computations in the free abelian category of an additive category $\mathbf{A}$. We show that the free abelian category is amenable to explicit computations whenever we can decide homotopy equations in $\mathbf{A}$. As some consequences of our investigations, we recover Dowker's explicit formula for the connecting homomorphism $\partial$ in the snake lemma, we find a universal sense in which $\partial$ is unique, and we give a refined version of the 5-lemma.