Theta-subsumption (θ-subsumption, or just subsumption) is a decidable relation between two first-order clauses that guarantees that one clause logically entails the other.
It was first introduced by John Alan Robinson in 1965 and has become a fundamental notion in inductive logic programming.
Deciding whether a given clause θ-subsumes another is an NP-complete problem.
[1] θ-subsumption is a weaker relation than logical entailment, that is, whenever a clause
This is still true when restricting the setting to pairs of Horn clauses.
[2] As a binary relation among Horn clauses, θ-subsumption is reflexive and transitive.
However, in every equivalence class of clauses that mutually θ-subsume each other, there is a unique shortest clause up to variable renaming, which can be effectively computed.
The class of quotients with respect to this equivalence relation is a complete lattice, which has both infinite ascending and infinite descending chains.
[3] θ-subsumption was first introduced by J. Alan Robinson in 1965 in the context of resolution,[4] and was first applied to inductive logic programming by Gordon Plotkin in 1970 for finding and reducing least general generalisations of sets of clauses.
[2] Theorem provers based on the resolution or superposition calculus use θ-subsumption to prune redundant clauses.
[7] In addition, θ-subsumption is the most prominent notion of entailment used in inductive logic programming, where it is the fundamental tool to determine whether one clause is a specialisation or a generalisation of another.