I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-theoretic language: I'd like to do inference in a cartesian closed category presented by a finite set of generators and relations. I would be interested in any references on this topic.
I understand that inference in this setting is generally undecidable. However, I wonder whether there is any literature that either gives useful conditions under which exact inference is possible or proposes heuristic algorithms for approximate inference.