Metagol Save Abandoned

Metagol - an inductive logic programming system

Project README

THIS VERSION OF METAGOL IS NO LONGER UNDER DEVELOPMENT. IT HAS (MOSTLY) BEEN SUPERSEDED BY POPPER.

Metagol is an inductive logic programming (ILP) system based on meta-interpretive learning. If you use Metagol for research, please use this citation and cite the relevant paper.

Using Metagol

Metagol is written in Prolog and runs with SWI-Prolog.

The following code demonstrates learning the grandparent relation given the mother and father relations as background knowledge:

:- use_module('metagol').

%% metagol settings
body_pred(mother/2).
body_pred(father/2).

%% background knowledge
mother(ann,amy).
mother(ann,andy).
mother(amy,amelia).
mother(linda,gavin).
father(steve,amy).
father(steve,andy).
father(gavin,amelia).
father(andy,spongebob).

%% metarules
metarule([P,Q],[P,A,B],[[Q,A,B]]).
metarule([P,Q,R],[P,A,B],[[Q,A,B],[R,A,B]]).
metarule([P,Q,R],[P,A,B],[[Q,A,C],[R,C,B]]).

%% learning task
:-
  %% positive examples
  Pos = [
    grandparent(ann,amelia),
    grandparent(steve,amelia),
    grandparent(ann,spongebob),
    grandparent(steve,spongebob),
    grandparent(linda,amelia)
  ],
  %% negative examples
  Neg = [
    grandparent(amy,amelia)
  ],
  learn(Pos,Neg).

Running the above program will print the output:

% clauses: 1
% clauses: 2
% clauses: 3
grandparent(A,B):-grandparent_1(A,C),grandparent_1(C,B).
grandparent_1(A,B):-mother(A,B).
grandparent_1(A,B):-father(A,B).

In this program the predicate symbol grandparent_1 is invented (i.e. does not appear in the background knowledge nor in the examples).

Metarules

Metagol requires metarules as input. Metarules define the form of clauses permitted in a hypothesis and thus the search space.

Metarules are of the form metarule(Name, Subs, Head, Body). An example metarule is:

metarule(chain, [P,Q,R], [P,A,B], [[Q,A,C],[R,C,B]]).

Here the symbols P, Q, and R denote second-order variables (i.e. can unify with predicate symbols). The symbols A, B, and C denote first-order variables (i.e. can unify with constant symbols). Metagol will search for appropriate substitutions for the variables in the second argument of a metarule (Subs).

Users must supply metarules. Deciding which metarules to use is still an open (and hard!) problem. Some work in this area is detailed in the papers:

For learning dyadic programs without constant symbols, we recommend using these metarules:

metarule([P,Q], [P,A,B], [[Q,A,B]]). % identity
metarule([P,Q], [P,A,B], [[Q,B,A]]). % inverse
metarule([P,Q,R], [P,A,B], [[Q,A],[R,A,B]]). % precon
metarule([P,Q,R], [P,A,B], [[Q,A,B],[R,B]]). % postcon
metarule([P,Q,R], [P,A,B], [[Q,A,C],[R,C,B]]). % chain

Please look at the examples to see how metarules are used.

Recursion

The above metarules are all non-recursive. By contrast, this metarule is recursive:

metarule([P,Q], [P,A,B], [[Q,A,C],[P,C,B]]).

See the find-duplicate, sorter, member, and string examples.

Interpreted background knowledge

Metagol supports interpreted background knowledge (IBK), which was initially introduced in these papers:

IBK is usually used to learn higher-order programs. For instance, one can define the map/3 construct as follows:

ibk([map,[],[],_],[]).
ibk([map,[A|As],[B|Bs],F],[[F,A,B],[map,As,Bs,F]]).

Given this IBK, Metagol will try to prove it through meta-interpretation, and will also try to learn a sub-program for the atom [F,A,B].

See the droplast, higher-order, and ibk examples.

Metagol settings

You can specify a maximum timeout (in seconds) for Metagol as follows:

metagol:timeout(600). % default 10 minutes

Metagol searches for a hypothesis using iterative deepening on the number of clauses in the solution. You can specify a maximum number of clauses:

metagol:max_clauses(Integer). % default 10

The following flag denotes whether the learned theory should be functional:

metagol:functional. % default false

If the functional flag is enabled, then you must define a func_test predicate. An example func test is:

func_test(Atom1,Atom2,Condition):-
  Atom1 = [P,A,X],
  Atom2 = [P,A,Y],
  Condition = (X=Y).

This func test is used in the robot examples. This test checks that if Metagol can prove any two Atoms Atom1 and Atom2 from an induced program, then the condition X=Y always holds. For more examples of functional tests, see the robots.pl, sorter.pl, and strings2.pl files.

Publications

Here are some publications on MIL and Metagol.

Key papers

Theory and Implementation

Applications / other

Theses

  • A. Cropper: Efficiently learning efficient programs. Imperial College London, UK 2017

  • D. Lin: Logic programs as declarative and procedural bias in inductive logic programming. Imperial College London, UK 2013

Open Source Agenda is not affiliated with "Metagol" Project. README Source: metagol/metagol
Stars
177
Open Issues
3
Last Commit
2 years ago
License

Open Source Agenda Badge

Open Source Agenda Rating