Prolog2

Prolog2 is a machine learning and logic programming framework, that implements native second-order logic and SLD resolution. This is an extension of Meta-Interpretive Learning, which was first used in Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited

This project aims to allow for more complex formations of second-order clauses and resolution.

Defining second order clauses

Traditional meta-rules can be written simply by making predicate symbols start with upper case letters. We must define which variables will remain as variables when a new clause is created from this higher-order clause. We define these existentially quantified variables using curly braces like so: {X,Y}

P(X,Y):- Q(X,Y), {P,Q}. %Identity

P(X,Y):- Q(X,Z), R(Z,Y), {P,Q,R}. %Chain

P(X,Y):- Q(X,Z), P(Z,Y), {P,Q}. %Tail Recursion

By default Existentially quantified varibles inside the {X,Y} notation are contrained so they can't become the same value or unify. This is intended to prevent unwanted recursion in meta-rules. If you want to remove this constraint EQ variables can be placed in []

P(X,Y):- Q(X,A), R(Y,B), {P,Q,R}, [A,B].
P(A,B), [A,B] % Meta fact

With this more flexible notation many we can create many more interesting second-order clauses for example, we can introduce certain constant predicate symbols either in the head or body to allow us to have greater control over the clauses that will be learnt. We can also create second-order clauses with only constant predicate symbols but existentially and universally quantified variables to denote the introduction of some constants

p(X,Y):- Q(X), R(Y), {Q,R}.

P(X,Y):- q(X,Y), R(Y), {P,R}.

p(X,Y):- q(X,Z), {Z}. %matching with this clause will create a new clause where Z is a constant

This can even be extended to using infix operators in second-order clauses

P(X,Y):- X > Y, Q(Y), {P,Q}.

P(X,Y):- Z is X + Y, Q(Z), {P,Q}.

Configuration Options

Configured in a JSON file (default: setup.json):

{
    "config" : {
        "max_depth": 20,
        "max_clause": 4,
        "max_pred": 2
    },

    "body_predicates" : [{"symbol" : "dad", "arity": 2},{"symbol" : "mum", "arity": 2}],
    "examples" : {
        "pos" : ["ancestor(ken,james)", "ancestor(christine,james)"],
        "neg" : []
    },
    "files" : ["examples/simple_family.pl"]
}

Running Prolog2

cargo run [[CONFIG_FILE] -- [OPTIONS]]

Arguments:

Examples:

# Interactive REPL using default setup.json
cargo run

# Run the ancestor learning problem
cargo run examples/ancestor/config.json

# Run ancestor and automatically find all solutions
cargo run examples/ancestor/config.json -- --all

# Just the --all flag with default config
cargo run -- --all

If the config file includes an examples field, Prolog2 will immediately attempt to prove the examples as a query and output any learned hypotheses. If examples is omitted, an interactive REPL is started where queries can be entered manually.

Step by Step Demonstration of New Clause Generation

1. First, we define a higher-order clause in our program P(X,Y):-Q(X,Y), {X}
2. Next, the prover reaches some goal that can match with the higher-order clause p(a,b)
3. This creates the binding {P/p, X/a, Y/b}
4. From this binding a new goal is generated, Q becomes an unbound variable _100(a,b)
5. Then, as this is a higher order clause, a new 1st order clause is created from the binding. The universally quantified variable X does not bind to a, but instead it transitions to an existentially quantified variable p(X,b):- _100(X,b)
6. Finally as the new clause has an unbound variable we add a constraint to our unification rules saying that _100 can not be bound to the value p

Example usage

Family relations

first, we lay out our background knowledge. What would have been called meta-rules is now better described as second-order clauses, where {P,Q} denotes that P and Q are variables which are existentially quantified, meaning they will become constants in new clauses derived from these meta rules.

The usage of the directive body_pred here tells the program that goals with variable symbols can match clauses of that symbol and arity.

mum(tami,james).
mum(tami,luke).
mum(christine,tami).
dad(ken,adam).
dad(adam,james).
dad(ken,saul).
dad(ken,kelly).
dad(adam,luke).

P(X,Y):-Q(X,Y), {P,Q}.
P(X,Y):-Q(X,Z),P(Z,Y), {P,Q}. % Tail Recursion

We must then define our learning parameters in a config file

{
    "config" : {
        "max_depth": 10,
        "max_clause": 4,
        "max_pred": 1,
        "debug": false
    },
    "body_predicates" : [
        {"symbol" : "dad", "arity": 2},
        {"symbol" : "mum", "arity": 2}
    ],
    "examples" : {
        "pos" : ["ancestor(ken,james)", "ancestor(christine,james)"],
        "neg" : []
    },
    "files" : ["examples/ancestor/family.pl"]
}

Then we can execute the binary with an argument for the path of the config file

$ target/debug/prolog2 examples/ancestor/config.json -- --all
TRUE
ancestor(Arg_1,Arg_2):-dad(Arg_1,Arg_4),ancestor(Arg_4,Arg_2).
ancestor(Arg_1,Arg_2):-dad(Arg_1,Arg_2).
ancestor(Arg_1,Arg_2):-mum(Arg_1,Arg_4),ancestor(Arg_4,Arg_2).
ancestor(Arg_1,Arg_2):-mum(Arg_1,Arg_2).

TRUE
ancestor(Arg_1,Arg_2):-pred_1(Arg_1,Arg_4),ancestor(Arg_4,Arg_2).
pred_1(Arg_1,Arg_2):-dad(Arg_1,Arg_2).
ancestor(Arg_1,Arg_2):-pred_1(Arg_1,Arg_2).
pred_1(Arg_1,Arg_2):-mum(Arg_1,Arg_2).

TRUE
ancestor(Arg_1,Arg_2):-pred_1(Arg_1,Arg_2).
pred_1(Arg_1,Arg_2):-ancestor(Arg_1,Arg_4),pred_1(Arg_4,Arg_2).
pred_1(Arg_1,Arg_2):-dad(Arg_1,Arg_2).
pred_1(Arg_1,Arg_2):-mum(Arg_1,Arg_2).

FALSE

Map

map([],[], P).

map([H1|T1], [H2|T2], P):-
    P(H1,H2),
    map(T1,T2,P).

double(X,Y):-
    Y is X + X.

{
    "config" : {
        "max_depth": 10,
        "max_clause": 0,
        "max_pred": 0,
        "debug": false
    },
    "body_predicates" : [],
    "files" : ["examples/map/learn_map_double.pl"]
}