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.
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.