Inference in typed lambda calculus theories
At least the problem of whether 2 terms are equal modulo the theory of Cartesian Closed Categories (or $\beta\eta$ conversion) is decidable, because (in part) of the normalization property.

Another, more categorical way to see this is by extracting a conversion algorithm through normalization by evaluation which gives decision procedures for equality in categories which can naturally be embedded in the presheaf or sheaf category over sets.

See e.g. Altenkirch, Dybjer, Hoffmann &amp; Scott, Normalization by Evaluation for Typed Lambda Calculus with Coproducts

for the version with products and coproducts (the version for just CCCs without coproducts can be found in the references).

An account which gives examples of implementations can be found here.

Solving more complex questions than conversion, or solving conversion questions in the presence of datatypes like the natural numbers becomes undecidable rather quickly. I'm not aware of much work on algorithms for such systems, which I would be interested in as well. One could try simply encoding the equational theory into a first-order logic prover like Vampire, but I don't know how well that would work. It would be an interesting experiment!