Non Monotonicity/Defeasibility Strategies and Other Stuff

General
27

Yes, that is just the kind of modification I’m talking about. Nice and simple, isn’t it?

Btw, this is the vanilla part in Louise:

prove(true,_K,_MS,_Ss,Subs,Subs):-
    !.
prove((L,Ls),K,MS,Ss,Subs,Acc):-
    prove(L,K,MS,Ss,Subs,Subs_)
    ,prove(Ls,K,MS,Ss,Subs_,Acc).
prove((L),K,MS,Ss,Subs,Acc):-
    L \= (_,_)
    ,L \= true
    ,clause(L,K,MS,Ss,Subs,Subs_,Ls)
    ,prove(Ls,K,MS,Ss,Subs_,Acc).

The differences with solve/1 in your comment are a) the two guard literals in the last clause, b) the call to the custom clause-fetcher clause/7, and c) some additional arguments.

The custom clause-fetcher is necessary because we want to resolve the clauses of the program derived so-far with new clauses, and with second-order clauses. This is what ultimately makes the proof an inductive one. You can omit this custom fetcher and use clause/2 instead if you write every induced clause to the dynamic database, and then remove it when the proof fails, etc, but while that would make the meta-interpreter simpler, the whole program would be a bug-ridden mess that would be much harder to understand. I know because an earlier version did just that and it was an endless pain in the entailment.

The additional arguments are there to store the set of inducible symbols (Ss) the set of second-order clauses (Ms) and two accumulator variables (the last two arguments) necessary to return the induced clauses at the end of the proof. These would also collect abduced atoms in the abductive modification I describe above. Again, if you wanted to keep everything in three lines and ten literals, plus the cuts, you could write everything to the dynamic database, but, why? That would make it all a lot more painful to follow the program.

Of course the main attraction to the inductive meta-interpreter above is that it’s inductive, not that it’s vanilla. With impeccable reviewer style you focused on the part of the claim that was least consequential :stuck_out_tongue:

But if you think that an inductive Prolog meta-interpreter can be written that is simpler than the one above, and that is “more vanilla”, please go ahead and demonstrate. I for one would be very curious to see what that looked like.