It depends on what you mean by “ILP”. The approach I discuss above, Meta-Interpretive Learning (abbreviated as MIL) is really a second-order form of SLD-Resolution. Note that I say “SLD” not “SLD(NF)”. No Negation As Failure! At least not in principle.
The nice thing about this framework is that it is fully reducible to first-order SLD-Resolution. That’s great because then we don’t need to prove soundness and completeness. Our framework inherits the soundness of SLD-Resolution and its completeness (i.e. the Subsumption Theorem and the Refutation Completeness). In the end, whatever claim we can make about MIL we can also make about SLD-Resolution.
What remains is to define the inductive setting, because we want to do induction. In the Standard Setting for ILP we have background knowledge B and positive and negative examples E+ and E-, and we want to find a logic program hypothesis H, such that:
- B ∪ H ⊨ E+
- ∀ e⁻ ∈ E⁻: B ∪ H ⊭ e⁻
In MIL, we have the same assumptions but with some restrictions and some extensions:
First, the background knowledge B consists of two components:
- B¹ is a set of first-order definite program clauses.
- B² is a set of second-order datalog program clauses.
- E+ and E- are sets of Horn goals (i.e. “facts”).
So to answer your question about datalog or not, B² is datalog, so there’s no function symbols; if we need functions we use a technique called “flattening” from the early days of ILP, which replaces each first-order term in an argument of a literal with a new body literal. For example, p(f(X), ...) becomes p(X,...) :- f(X), ... etc.
As to SLD(NF) resolution, in principle B¹ is definite. No NaF. In practice most systems implicitly allow it so you’ll find NaF in many MIL background knowledge sets, but the properties of the framework are only nice without it.
Finaly, it’s important to note that E+ are allowed to be non-ground. In practice most of the time they’re not, but in some cases they are and that opens various interesting possibilities. I have never seen or used E- that were not fully ground.
Given B¹, B², E+ and E- as above we now want to learn a hypothesis, H, such that:
- B² ⊨ H
- B ∪ H ⊨ E+
- ∀ e⁻ ∈ E⁻: B ∪ H ⊭ e⁻
So basically the same as with the Standard Setting, but with the added assumption that H is entailed by the second-order background knowledge. Or, in other words, H is a specialisation of the second-order background knowledge.
The great thing about this is that if the three conditions above apply, then we can find H by SLD-Refutation of the positive examples in E+ and this is guaranteed by the soundness and completeness of SLD-Resolution. Negative examples are used to discard hypotheses that violate the third condition, which again we can find by SLD-Refutation of E-.
The way all this is implemented is explained in my earlier reply to @jan. Since our framework is SLD-Resolution, we learn H by SLD-Refutation of E+ with B¹ and B². Importantly, we can also allow Resolution of H with ittself, which enables the learning of arbitrary recursion, including left-recursion. This is possible by switching to SLG-Resolution, or removing the ability of H to resolve with itself. In all cases we also limit the number of times a second-order definite clause can resolve with itself, which is normally infinite.
I hope this addresses your concerns regarding decidability. While it’s true that Turing complete languages are not decidable, that’s in the general case. Obviously we can run any number of logic programs in a Prolog interpreter so the undecidability of FOL and Turing-Completeness are Prolog are not a real impediment in doing practical work. And if theoretical completeness is a problem, we can always stipulate that a depth limit is applied in which case the framework is complete up to a depth of K. I find that this satisfies the most demanding theoreticians. Your mileage may vary!
Please let me know if you have more questions and Happy Easter.