Next: The Contradiction Backtracing Algorithm Up: COMP9417 Project Shapiro's Model Previous: COMP9417 Project Shapiro's Model



This section is a brief introduction and overview of Machine Learning, Logic Programming, Inductive Logic Programming, and Shapiro's Model Inference System.

Source code for the applets used in this document can be found at: (I've merged it with my thesis work).

Logic Programming

Logic Programming is the area that broadly includes languages based in a fairly direct way on a logic, which is usually taken to be classical first-order Horn-clause logic. These semantical foundations are usually augmented with negation-as-finite-failure, meta-programming facilities (e.g. call/1, asserta/1, retract/1) and type, mode, and module systems. Prolog is the original such language, dating from the early 1970's, and lacks all such niceties except the first two.

A tutorial introduction to Prolog can be found in [CM81], and [Llo87b] provides a thorough treatment of the semantics of a purified version of the language.

In the following, we assume familiarity with logic programming. The specialised terminology of this field is described in Appendix A.

Proof by Refutation

Prolog uses a form of resolution [Rob92] to execute logic programs. Restricted to Horn clauses, this proof technique uses the following rule of inference (a reworded version of [Sha81]):

Let $C_1 = \leftarrow r_1, q_1, ..., q_n$ (a definite query), $C_2
= r_2 \leftarrow s_1, ..., s_n$ (a definite clause) be sentences in $L$. Provided that $r_1$ and $r_2$ have a most general unifier $\theta$ (i.e. $P = r_1\theta = r_2\theta$), then the resolvent of these two clauses is $(\leftarrow q_1, ..., q_n, s_1, ..., s_n)\theta$, and $P$ is termed the atom resolved upon. $C_1$ is called the left component, and $C_2$ the right component.
The aim is to derive the empty clause, written $\Box$, which is interpreted as ``contradiction''. This means that the query is inconsistent with the theory, from which we conclude that the negation of the query is in fact consistent with it. What's more, substitutions for the variables in the query that satisfy the latter are computed during the search for a refutation.

Horn clauses are particularly useful, as they have a very natural algorithmic interpretation; they have the flavour of the procedures found in imperative langauges. The output of such an executation is a sentence that satisfies the constraints asserted by the program, or failure if no such solution is found. In $r \leftarrow q_1, ..., q_n$, $r$ is called the head of the clause and $q_1, ..., q_n$ the body. To execute the head, each conjunct of the body must be executed.

Refutation proof trees1 provide a way of visualising the logical aspect of executing a Prolog program, in contrast to the procedural (or operational) view that a debugger for an imperative language (such as C) would provide. The completed refutation tree should be read as ``because all the children are true, the parent is true in the context of the theory T''.

Your browser does not support Java applets.

Inductive Logic Programming

The goal of Inductive Logic Programming is to induce a compact, generalised, understandable-by-humans description of a set of facts in a very expressive formal language. The term was coined by Muggleton in 1991 [Sam93], but the field had been under active investigation for a long time before that. An overview of rule-learning (of which ILP is an instance) can be found in [Mit97, Chapter 10], and a substantial amount of ILP theory is presented in [NCdW97].

Given the gamut of programming languages, we might ask what it is about logic programming that makes it a good target for induction. We defer answering this question until we have presented the Model Inference System (Section 5) so that we have a point of reference.

Alternatively, it may be asked why a more expressive formal language such as full first-order logic is not employed. The main reason is efficiency: a theory induced by an ILP system is effectively and efficiently executable via a Prolog-like theorem prover, and does not require a massively non-deterministic search to determine whether a particular statement follows.

There is a plethora of ILP systems, e.g. FOIL [QCJ93], MARVIN [SB86], Progol [Mug95], and many variations on some core ideas. The two fundamental approaches taken to the induction problem are to exploit the properties of the description language (e.g. MIS) and to use a statistical model (e.g. FOIL). Any effective ILP system needs to combine them in some way: the former can greatly increase efficiency by better structuring the search space, and the latter is mandated by noisy (real-world) data. Again, we discuss these after presenting MIS.

In order to provide some intuition about ILP, the following points contrast it broadly with decision tree inducers [Mit97, Chapter 3 and 10]:

Philosophical Concerns

Abstractly, we might pose the question: just what is a valid inductive generalisation? From a classical philosophical viewpoint3, a satisfactory answer to this question is needed if we are ever to escape the ``I think, therefore I am'' solipsism of Descartes and be assured that it is possible to make valid assertions about the inter-subjective realm.

Hume [Hum85] argued quite forcefully in the eighteenth century that there can be no logically sound reason to generalise from experience to univerally true statements. The essence of his argument is that we must assume that nature is uniform if we were to grant validity to such statements, and that such an assumption cannot be verified indepedently of experience.

So, are we completely stuck? Surely not. In the context of machine learning we're simply looking for good descriptions that fit the data we have available - there is no inherent claim for universal generality here. Indeed, completeness is not always in itself desirable - a topic we take up in Section 3.

In contrast to empirical scepticism, we can simply assume that generalisations are necessary (perhaps as an aid to comprehending large amounts of data) and move along to the question of what a good way of discovering them is. In concert with this, we need to know what the requirements for effective learning are; can we, for example, learn simply by being exposed to positive examples of a concept?

While the former question is a matter of research, the latter one and others similar to it have been studied in some detail by computational learning theorists - see [JORS99] for an in-depth coverage of such.

Shapiro adopts the learning-in-the-limit model [Gol67] in order to prove various properties of his algorithms. Informally, the idea is that, given a presentation of facts in an observation language $L_o$, the learner outputs a series of conjectures drawn from a hypothesis language $L_h$ that eventually converges to a finite description of them4. Note that there is no introspection requirement: the learner never realises that it has happened upon the correct description. Thus, the crux of Hume's argument - that we cannot establish uniformity - is side-stepped.

In the context of this model, both positive and negative examples are required; without negatives we could trivially output the everywhere-true program, and similarly for the no-positives case.

An Overview of the Model Inference System

The Model Inference System, by Ehud Y. Shapiro [Sha81,Sha83] is an instance of the class of incremental generalise/specialise algorithms, which have the skeleton shown in Figure 1.

Figure 1: The skeleton of a generalise/specialise learner.

Shapiro formalises the Model Inference Problem as follows [Sha81]:

Suppose we are given a first order language $L$ and two subsets of it: an obervational language $L_o$ and a hypothesis language $L_h$ with $\Box \in L_o \subset L_h \subset L$. In addition, assume that we are given an oracle for some unknown model $M$ of $L$. The Model Inference Problem is to find a finite $L_o$-complete axiomatization of $M$.
Unpacking this definition, we have the following:

MIS itself consists of two parts: roughly, a systematic way of finding bugs in programs (discussed in Section 2), and a search for fixes for these bugs (Section 3).

Both of these exploit the clean semantics of the pure Horn Clause core of Prolog, and hence run into difficulties with the non-logical parts of the language (e.g. the cut - !/0, unsound unification and the incompleteness of Prolog's proof strategy). Indeed, learning with the cut has since been shown to be difficult [BGT93].

Some further a priori observations:

next up previous
Next: The Contradiction Backtracing Algorithm Up: COMP9417 Project Shapiro's Model Previous: COMP9417 Project Shapiro's Model
Peter Gammie