[falsissime]

(It seems one needs to go into a post directly to be able to reply more rapidly. The delay seems to be reserved for the thread-mode.)

Before sending an e-mail, check https://www.softwarepreservation.org/projects/prolog/ there are so many original sources now online that help to reconsider some perceptions. In particular, the Prolog I manual is there, but in a very bad shape (bad scan from a used up chain printer, probably a 3203, all caps, no accents ...).

[YeGoblynQueenne]

>> (It seems one needs to go into a post directly to be able to reply more rapidly. The delay seems to be reserved for the thread-mode.)

Oh, right, good catch!

That's an amazing resource you linked me to. Thanks!

On the other hand, it's such an awful feeling some times that all the activity of the early years of logic programming has died out, that I've come to it too late, and that so many of the people who created the field are now retired or gone.

[falsissime]

> ... all the activity of the early years of logic programming has died out, ...

Of course, now there is activity of the current years! What else could we have now? If you look back, there was not only progress but also quite a lot of regress. Like, dif/2 in Prolog 0, then to stay submerged for so long, resurfacing in Prolog II and Mu etc. Errors in Prolog I, then abolished in DEC10 at the expense of incorrectness, only to resurface later on, but still not entirely recovered...

[YeGoblynQueenne]

Btw, the reason I want to write to Kowalski is not just the history of meta-interpreters. There's a question that only he may be able to answer. The question is about the Subsumption Theorem in Inductive Logic Programming (ILP).

Briefly stated, the Subsumption Theorem, as it's known today, is that a clause D is entailed by a logic program S if there exists a clause C that can be derived from S and such that C subsumes D.

Similar statements are also found in the logic programming literature, for example in Lloyd's Foundations of Logic Programming.

There's a bit of a mystery about the origins of the Theorem.

A series of similar papers by Ninenhuys-Cheng and de Wolf point out different definitions and apparent rediscoveries of the Theorem, and proofs of it, some of them mistaken, in the ILP literature. The paper I use as my reference is titled The Subsumption Theorem in Inductive Logic Programming: Facts and Fallacies. (http://homepages.cwi.nl/~rdewolf/publ/ilp/ilp95.pdf found in Ronald de Wold's webpage, here: https://homepages.cwi.nl/~rdewolf/).

That paper claims that the Theorem was probably first stated by R. C. T. Lee, in his 1967 doctoral thesis. It seems this information comes from Kowalski, in a paper that I can't access fully (cited in the Nienhuys-Cheng and de Wolf paper). However, the earliest statement, and proof, of a Subsumption Theorem that I could find is from Robinson's resolution paper, published in 1965, where subsumption is also defined. The Subsumption Theorem in Robinson's paper is slightly different than the one found in the ILP literature, in fact it looks to me like the modern version of the Subsumption Theorem is a corrolary of Robinson's one.

If I were to rephrase Robinson's Subsumption Theorem in more modern terms, what it says it as follows:

[Restated Subsumption Theorem] Let S be a finite set of clauses and C ≠ D be two clauses that are not in S and such that C ≼ D (C subsumes D). Then, S ∪ {C,D} is satisfiable if and only if S ∪ {C} is satisfiable.

So this statement is missing the explicit requirement for derivation of C from S, but if S ∪ {C} is satisfiable then C should be derivable from S by Resolution.

Now, R. C. T. Lee's thesis is not available anymore, it seems, and it wasn't available to Nienhuys-Cheng and de Wolf, either, so there's a lot of uncertainty around what, exactly, Lee stated and proved, and how it is similar or different to Robinson's Subsumption Theorem, and to subsequent statements of the Subsumption Theorem in ILP. Kowalski may be able to clarify the confusion.

I'm posting this in the very slim chance that you might have some intuition about all this, in which case I'd be grateful to hear it.