** Second-Order SLD-Resolution in Meta-Interpretive Learning **
Inductive Logic Programming (ILP) is the field that studies approaches to the machine learning of logic programs from examples and background knowldge. Meta-Interpretive Learning (MIL), the subject of this talk, is a new form of ILP capable of learnig arbitrary logic programs with recursion and with invented predicates from very few examples and without the limitations of earlier approaches. What distinguishes MIL from other ILP approaches is its use of second-order background knowledge and SLD-Resolution as a proof procedure.
In this talk I will go briefly over the short history of MIL and describe the different stages of its evolution in both theory and implementation. I will describe the emerging theoretical understanding of MIL as Second-Order SLD-Resolution and the theoretical and practical ramifications of this new understanding. I will sketch out a proof of the inductive soundness and completeness, and the efficiency, of Second-Order SLD-Resolution in MIL. I will discuss existing implementations of MIL and their ongoing application to practical problems such as generalised planning for robotics, and machine vision currently underway at the University of Surrey.
Finally, I will examine potential future applications to other classical AI tasks such as formal methods, verification and model checking. The talk is designed to be accessible to computer scientists with a background in logic and general knowledge of logic programming and machine learning.