Building a proof tree / collecting clauses in a refutation sequence

Help!
33

You’re right, this should not happen- it’s either a bug or there’s garbage left behind in the dynamic database. I’ll give it a try with a clean session.

Edit: your meta-intepreter from the SO question sure looks useful for quick debugging.

Edit: OK, I see what happened- you’re putting the entire program and background knowledge (BK) together in the _Ts variable, which is for the program alone, so if a successful refutation sequence exists for an example that includes a clause in the BK you will get that clause in the output.

The question is: where does a successful refutation sequence come from, that involves s/2? The answer is: from the positive example, s^2(foo) itself. prove_examples/6 asserts the positive examples in _Pos to the dynamic database. So there always is at least one refutation sequence for each example in _Pos that includes the example itself.

I can see this happening when I turn on logging with debug(remove_null):

% Proving positive example
% nat(s(s(foo))). 
% Called clause 4
% s(s(foo),foo). 
% Called clause 4
% s(s(s(foo)),s(foo)). 
% Called clause 7
% nat(s(s(foo))). 
% Proved positive example
% nat(s(s(foo))). 
% Collected clause indices
% [4,7].

Why are the positive examples added to the dynamic database. Are they not always entailed by the program? Yes, but there are some recursive clauses that were induced by resolution with the positive examples. This allows Louise to construct some recursive clauses, those that don’t need to self-resolve, but can be constructed by resolution of their recursive goals with positive examples. So the positive examples must be in the program database along with the rest of the program (which would have normally been learned by Louise) to act as a base-case for some recursions. This is part of why what I’m trying to do is so fiddly- and why I need to find all refutation sequences. If you look at the code, it should also explain why the examples in _Pos are asserted to the dynamic database (with a call to assert_program/3 and why this is done after the clauses in _Ts are asserted).

Edit 2: on second thoughts that doesn’t quite explain it- clause 4 (s/2) never resolves successfully so it shouldn’t be in the successful refutation sequence. There’s a bug for sure. Thanks for pointing it out :slight_smile:

Edit 3: For the time being, if you separate the program from the BK you get a result that makes sense:

?- _Ts = [(nat(X1) :- even(X1)), (nat(X2) :- odd(X2)), (odd(A):-s(A,B),even(B)), s(s(X3),X3), even(0), (even(s(X4)):-odd(X4))],
_BK = [],
_Pos = [nat(s(s(foo)))],
_Neg = [], 
_Ss = [nat/1],
prove_examples(_Ts, _Pos, _Neg, _BK, _Ss, _Ts_), print_clauses(_Ts_).
s(s(A),A).
nat(s(s(foo))).
true.
34

All of this is way over my head, but what exactly was your objection to using prolog_trace_interception/4?

You wrote,

but it seems like you might have misunderstood this. It shouldn’t need user interaction, depends how you define it I guess? From the docs:

If this predicate succeeds, the debugger assumes that the trace action has been taken care of and continues execution as described by Action.

This doesn’t turn on tracing, you turn on tracing, but replace the interactive debugger with what you really want. This, in combination with Examining the Environment Stack, maybe you don’t need to keep state in the dynamic database? Can’t tell for sure.

1 Like
35

I see, thanks- I did absolutely misunderstand that. I saw the “trace” “notrace” around “Goal” in record_trace/1 and I thought it’d just start the tracer. That could work actually. I’ll play around with it more.

I’m willing to bet I’m shorter than you so there’s more stuff way over my head :stuck_out_tongue:

36

Ha! but anyway if you do something please follow up. I have never used these predicates and now I just read the docs and made an educated guess.

37

And a very good guess it was. I’m always confused by those sections of the Swi documentation that discuss hooks and so on, the sneaky indirection reminds me of the time I worked at web development and my mind recoils from the thought.

I’ll post stuff when I have something- promise :slight_smile:

39

Yes, this is right- the refutation sequence that includes s/2 is failed, because it doesn’t terminate in the empty clause. Like I say above, this is a bug in my code. s/2 should not be output!

More precisely I think in SLD resolution the C_i are a mix of resolvents and clauses from the program database. I’m going by Lloyd’s definition of an SLD-Derivation (see the chapter on Definite Programs, section 7, Soundness of SLD-Resolution; I have the second edition of Lloyd):

Let P be a definite program and G be a definite goal. An SLD-derivation of P U {G} consists of a (finite or infinite) sequence G0 = G, G1, … of goals, a sequence C1, C2, … of variants of program clauses of P and a sequence θ1, θ2, … of mgu’s such that each Gi+1 is derived from Gi and Ci+1 using Θi+1.

Then an SLD-refutation of P U {G} is defined as an SLD-derivation of P U {G} which has the empty clause as the last goal in the derivation.

So you are correct that an SLD-derivation includes resolvents and my bad for not making that clear. But my program should only output clauses from the program database and then again only the clauses of the predicates defined in the variable _Ss in the input to prove_examples/6.

Looking at the resolvents is another possibly interesting thing to do and so is looking at the mgu’s, but for the time being my purpose is to extract the clauses of the program used in a refutation.

42

Directly from Lloyd :slight_smile:

The definition of SLD-resolution is from page 41 in the second edition of Lloyd’s book. I did not copy the definition of an SLD-refutatin but rather re-stated it for brevity. Lloyd doesn’t specify any termination condition and indeed states that an SLD-derivation may be infinite. Is that what you mean?

Yes. Are we going back and forth on very subtle matters of terminology here? I was hoping that my intent with the program was clear at this point. Have I achieved maximum confusion instead? If so, I apologise and am happy to help reduce the confusion if you want.

Is the terminological confusion rooted in my use of the expression “refutation sequence”? I get that from Foundations of ILP, by Nienhuys-Cheng and De Wolf. It may be non-standard terminology, the book has a tendency to come up with new definitions (and also new proofs) etc. so it may be confusing. But that should be par for the course for textbooks so old that they are at the edge of -at the time- new research.

In the past I’ve tried both approaches: using precise terminology, lifted from a textbook or other authoritative source; and describing things in an informal manner. Both approaches have their pifalls. Even formal terminology can be subtly different between authors and that seems to lead to confusion not much reduced with respect to “winging it” with informal terminology. Please say which way you prefer to communicate, I’m primarily trying to get my point across and am not wedded to any particular way of communication - anything that works, works.

44

The term “super goal” is new to me and I’m scratching my head trying to figure out where it fits with what I know, so it’s possible it refers to something about which I don’t know anything. Are you talking about resolution between non-clauses? I haven’t really studied that much since I’m very focused on approaches that can be implemented in Prolog. Does Prolog have a concept of super-goal?

Could you give an example of a super goal?

46

Thanks for clarifying- I always thought of “super goals” as simply “goals” (with many literals). As I say above, this is the result of my focus on Prolog where super goals are natural.

Edit: On second thoughts… Nienhuys-Cheng and De Wolf define a “definite goal” as follows:

Defintiion 7.1 A definite program clause is a clause containing one positive and zero or more negative literals. A definite goal is a clause containing only negative literals. A Horn clause is either a definite program clause, or a definite goal.

So I actually get my definition of goals as clauses with multiple negative literals, i.e. what you call “super goals”, from FoILP. I’ll have a look to see how Lloyd defines them.

Edit 2: Right. Lloyd also defines goals as having multiple body literals potentially:

Definition A definite goal is a clause of the form ← B1, …, Bn that is, a clause which has an empty consequent. Each Bi (i=1,… n) is called a subgoal of the goal.

Er, I don’t see him saying “supergoal” anywhere but if there’s “subgoals” then there’s “supergoals”, OK :slight_smile:

49

That’s a nice intuition again.

Depends on how you see it. In a sense, much better than any other machine learning approach, because Inverse Resolution (IR) is neither a) limited to classification nor b) trained by some kind of gradient optimisation. Pretty much every other machine learning approach, outside of ILP, is at least one of those things and deep learning is really much better than anything else that is one or both of those things, so it’s hard to justify continued research on, say, Support Vector Machines or Bayesian learners when you have something that can do what they do 10 times better.

ILP is a different beast altogther: it’s a program learning approach, so it can do a lot more than just classification; and since programs, in the general sense, are discrete, continuous optimisation techniques can’t really work. IR itself is probably the most popular ILP approach, historically. Personally, I find that it’s surpassed today by Meta-Interpretive Learning (MIL), which can for the first time realise two important promises of ILP, the ability to learn recursive programs without any meaningful limitations (e.g. older systems were limted to learning recursive programs of a particular structure, like one recursive clause with a specific number of literals and one base-case clause again with a specific number of literals) and predicate invention again without any meaningful limitations. In particular the way that MIL performs predicate invention is really something new- there’s never been any other approach in the history of ILP that could even come close. Basically, predicate invention with MIL is sound and complete for datalog (and also for definite programs in general, but there we stumble on theoretical decidability issues).

In any case, work did not cease in Logic Programming because of deep learning. Why should it cease on Inductive Logic Programming? As far as I’m concerned deep neural nets are still incapable of doing reasoning, powerful classifiers though they are. And then there’s issues like tragic sample efficiency, inability to use background knowledge, “black box” incomprehensible models, overfitting, etc etc. There’s a lot of hype, but ILP and MIL actually goes a very long way towards addressing many of the limitations of deep learning.

Save two. One, MIL has atrocious time complexity- it’s exponential in the number of clauses in a target theory (which however is addressed by my own work). And two… what is a Horn clause again? :slight_smile: (i.e. there is not a rich pool of computer scientists with deep background in FOL and logic programming to draw from).

Full disclosure: Stephen Muggleton is my thesis advisor and I work on MIL, so I’m liable to ranting about it a bit :wink:

You’re right. I hadn’t thought of that. Well if I get something working it could certainly be the right tool for that job. More wind in my sails!

1 Like
50

Did you ever get this completed?

I saw prove_examples.pl (12.8 KB). Is that the final code?

Just curious. :slightly_smiling_face:

51

This is certainly way after the original question, but for the sake of anyone else who finds this thread and is looking for solutions to a similar problem, I want to point out the prolog_wrap library as a way to do targeted execution tracing, if you don’t want to get into the trace hook machinery. It’s what powers the trace/1,2 tracepoint system (which, as the docs mention, is completely different from the tracer), and it works even if debug mode is turned off - important, since some programs just won’t work with debug mode on (due to tail recursion or similar), and the tracer, even when completely automated by the hooks, won’t function outside debug mode.

53

Hi Eric! Wow, it took me 5 months to reply, that’s too long even for me- sorry!

The answer is: I didn’t take that any further. I find it harder and harder to justify work that isn’t directly tied to my (attempted) publications and that one wasn’t. It’ll get done at some point in the future, hopefully. But, for the time being, that should be considered the “final” version, so yes.

1 Like
54

Actually it was only 7 days. :smiley: