Implementing abduction over first order theories

I am interested in implementing abduction over a full first order theory ie it may be non-Horn. (Aside: Almost all the references I've seen for abduction operate over Horn theories eg "Modeling Abduction over Acyclic First-Order Logic Horn Theories in Answer Set Programming: Preliminary Experiments". Is there a reason for this other than lack of minimal hypotheses?) Are there frameworks that might be suitably modified for my purposes? Alternatively, does anyone know of a way of coaxing a SMT solver into perhaps giving me something close to what I need?

thanks!

You could use an SMT solver inside a counterexample-guided inductive synthesis loop to learn an expression that fits. The paper below does something similar. If you aren't interested in finding the weakest expression, you could save on computational costs by using templates.

• Albarghouthi, Aws, Isil Dillig, and Arie Gurfinkel. "Maximal specification synthesis." ACM SIGPLAN Notices. Vol. 51. No. 1. ACM, 2016.

StackExchange Computer Science Q#77009, answer score: 2