Inductive Logic Programming (https://en.wikipedia.org/wiki/Inductive_logic_programming) find hypothesis theory H for background theory B and set of examples E. ILP algorithms and implementations usually expects, that H, B, E are logic programs - set of Horn clauses and not general FOL or HOL theories. This approach is generalized to the HOL logic programs as well, e.g. in http://andrewcropper.com/pubs/ijcai16-metafunc.pdf.
My question is - are there efforts to formulate induction/ILP for general theories. Apparently, the algorithm does exist and the problem is undecidable, but still - are there some heuristics, some approximate approaches, some more or less rigorous work for such generalization? Both - for full FOL and HOL?
E.g. references wiki articles mentions the method of inverse entailment - I see that that approach is general enough - it requires the computation of the most conscise (e.g. Occams razor principle - with the minimal Kolomogorov or other complexity) set of consequences in some depth.
Actually - ILP may be the Holy Grail of AI: 1) it can learn general policies from the specific policies and hence - implement generalization and transfer learning, e.g. in reinforcement learning; 2) it can learn the program which from background knowledge computes the set of input-output patterns (in more or less general form) and hence - solve the program synthesis task.