Oops, sorry, I just saw your comment.

I'm working on a paper about this but I guess that won't be "layman terms". Let me try to give a simple explanation. I'm assuming "layman" means "layman programmer" :)

In the simplest of terms that I think can be understood by a layman programmer then, second-order SLD-Resolution in Meta-Interpretive Learning (the method I discuss above) doesn't need to search for a program in a large program space because it is given a program, a higher-order logic program that is specialised into a first-order program during execution.

Without having to know anything about the execution of Prolog programs you can think of how a program in any programming language is executed. The execution doesn't need to search any program space, it only needs to calculate the output of the program given its input. The same goes for the execution of a Prolog program, but here the result of the execution is a substitution of the variables in the Prolog program. In the case of a higher-order program, the substitution of variables turns it into a first-order program (that's what I mean when I say that the higher-order program is "specialised").

Here's an example (using Louise, linked above). The following are the training examples and first- and second-order background knowledge to learn the concept of "even". The terminology of "background knowledge" is peculiar to Inductive Logic Programming, what it really refers to is the higher-order program I discuss above:

?- list_mil_problem(even/1).
Positive examples
-----------------
even(4).

Negative examples
-----------------
:-even(3).

Background knowledge (First Order)
----------------------------------
zero/1:
zero(0).

prev/2:
prev(1,0).
prev(2,1).
prev(3,2).
prev(4,3).

Background knowledge(Second Order)
----------------------------------
(M1) ∃.P,Q ∀x: P(x)← Q(x)
(M2) ∃.P,Q,R ∀.x,y: P(x)← Q(x,y),R(y)

true.

Given this problem, Louise returns the following first-order program:

?- learn(even/1).
even(A):-zero(A).
'$1'(A):-prev(A,B),even(B).
even(A):-prev(A,B),'$1'(B).
true.

If you squint a bit you'll see that the clauses that make up this first-order program are the clauses of the second-order "background knowledge", with their existentially quantified variables substituted for predicate symbols: 'even', 'zero' and 'prev'. Those symbols are taken from the first-order background knowledge (i.e. the first-order subset of the higher-order program) and the examples. There is an extra symbol, '$1', which is an invented predicate symbol, not found in the background knowledge or examples and instead automatically generated during execution. If you squint a bit harder you'll see that the clause '$1'(A):-prev(A,B),even(B). with that symbol in its head is a definition of the concept of "odd". So Louise learned the concept of "even" by inventing the concept of "odd".

The natural question to ask here is, I suspect, couldn't you do the same thing just by filling-in the blanks in the second-order clauses in the background knowledge, as if they were dumb templates? You could, and in fact that's the done thing in inductive program synthesis. But that's when you end up searching the space of all logic programs (i.e. the space of sets of first-order clauses). There's a whole bunch of programs that you could construct that way and you'd have to decide which to keep. To do that you'd have to construct each of them, so you'd have to construct the powerset of all constructible clauses. Powersets grow exponentially with the size of their base set, leading to combinatorial explosion. The win of using SLD-Resolution is that it only needs to find substitutions of variables, which can be done efficiently, and it only returns those substitutions of the variables in the second-order program that prove the positive examples (and disprove the negative ones). So it's always right (SLD-Resolution is sound and complete).

>> I’m also curious if this scales to real world problems.

Depends on what you mean "real world problems". The largest program I've learned with Louise is a 2500-clause program, but that's for a dumb problem that only serves as a benchmark (the problem is to find every way to go from a point A to a point B on an empty grid-world; it's surprisingly combinatorially hard and other methods die before they get anywhere near the 2500 clause mark; because the program search space blows up immediately).

In truth, real-world Prolog programs rarely need to be much bigger than a handful of clauses, like five or six. At that point, like in any programming language, you break your program up into smaller sub-programs, and those can be learned easily enough (and not just by second-order SLD-Resolution, to be fair). The challenge is to figure out how to do this breaking-up automatically. Meta-Interpretive Learning with Second-Order SLD-Resolution can do it up to a point, with predicate invention, as in the example above and also because any program learned can go directly into the "background knowledge" to be reused in a new learning session. But that still hasn't been done in a systematic manner.

Right now I'm working on a project to grant autonomous behaviour to a robot boat used in search-and-rescue missions. This is a fairly large problem and there are certainly challenges to do with efficiency. In fact efficiency is the main challenge. But from where I'm standing that's an engineering challenge.

So to answer your question: oh yes ^_^