This answer builds on those of F. G. Dorais and Joel David Hamkins to answer your "specific question", the question left open by them, namely whether the theory of abelian categories is decidable.
The answer is still no.
Even the following more limited family of problems is undecidable:
Given words $r, r_1,\ldots,r_m$ in $x_1,\ldots,x_n$ (i.e., each $r_i$ is a finite product of the $x_i$ and their inverses), decide whether it is true that whenever the $x_i$ are interpreted as automorphisms of an object $M$ in an abelian category, $r_1=\cdots=r_m=1_M$ implies $r=1_M$.
If the answer to the corresponding instance of the word problem for finitely presented groups is yes, then the answer to this abelian category question is yes. Conversely if the answer to the word problem instance is no, then we can construct the finitely presented group $G = \langle x_1,\ldots,x_n | r_1,\ldots,r_m \rangle$, form the group ring $\mathbb{Z}G$, and let $M$ be $\mathbb{Z}G$ as a module over itself, which shows that the answer to the abelian category question is no too.
So if there were an algorithm to decide this family of abelian category problems, there would also be an algorithm to decide the word problem for finitely presented groups. But P. S. Novikov proved in 1955 that the latter algorithm does not exist.
